perm filename LISP.CMP[TIM,LSP]1 blob
sn#688869 filedate 1982-11-29 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00013 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 Comparison of LISPS
C00004 00003 The FRANZ code
C00026 00004 The ELISP code
C00047 00005 (FILECREATED " 5-Jul-82 12:52:49" <CL.BOYER.LISPS>IREWRITE..4 14918
C00072 00006 The Maclisp Code
C00093 00007 The FRANZ tests
C00106 00008 The ELISP test
C00107 00009 Interlisp bcompl blocklib swap and noswap
C00110 00010 Interlisp bcompl no blocklib swap and noswap
C00114 00011 Maclisp
C00120 00012 Interlisp (Dolphin and Dorado)
C00151 00013 The INTERLISP VAX test
C00154 ENDMK
C⊗;
Comparison of LISPS
This page contains a summary. Subsequent pages contain the
code used and documentation of the tests. All the code was compiled.
Non GC time (seconds) GC time Total
MACLISP (2060) 8.5 5.3 13.8
UCILISP (2060, (nouuo nil)) 9.3 4.7 14
INTERLISP (bcompl, blklib, swap, 2060) 11 6 17
ELISP (2060) 11 7 18
INTERLISP (bcompl, blklib, noswap, 2060) 11 7.5 18.5
INTERLISP (Dorado, bcompl, blklib) 18 11 29
FRANZ (all localf, VAX-780) 21 18 39
INTERLISP (bcompl, no blklib, noswap, 2060) 39 7 46
FRANZ (translink=on, VAX-780) 37 17 54
INTERLISP (bcompl, no blklib, swap, 2060) 64 6 70
INTERLISP (VAX-780) 80 3 83
ZETALISP (LM-2, 1meg, gc-on) breakdown not available 97
FRANZ VAX-780 (translink=nil) 130 18 148
INTERLISP (Dolphin, 1meg, bcompl, blklib) 132 35 167
The FRANZ code
(declare (special unify-subst temp-temp))
(declare (localf
add-lemma add-lemma-lst apply-subst apply-subst-lst falsep one-way-unify
one-way-unify1 one-way-unify1-lst rewrite rewrite-args rewrite-with-lemmas
tautologyp tautp trans-of-implies trans-of-implies1 truep))
(defun add-lemma (term)
(cond ((and (not (atom term))
(eq (car term)
(quote equal))
(not (atom (cadr term))))
(putprop (car (cadr term))
(cons term (get (car (cadr term))
(quote lemmas)))
(quote lemmas)))
(t (error (quote add-lemma-did-not-like-term)
term))))
(defun add-lemma-lst (lst)
(cond ((null lst)
t)
(t (add-lemma (car lst))
(add-lemma-lst (cdr lst)))))
(defun apply-subst (alist term)
(cond ((atom term)
(cond ((setq temp-temp (assq term alist))
(cdr temp-temp))
(t term)))
(t (cons (car term)
(apply-subst-lst alist (cdr term))))))
(defun apply-subst-lst (alist lst)
(cond ((null lst)
nil)
(t (cons (apply-subst alist (car lst))
(apply-subst-lst alist (cdr lst))))))
(defun falsep (x lst)
(or (equal x (quote (f)))
(member x lst)))
(defun one-way-unify (term1 term2)
(progn (setq unify-subst nil)
(one-way-unify1 term1 term2)))
(defun one-way-unify1 (term1 term2)
(cond ((atom term2)
(cond ((setq temp-temp (assq term2 unify-subst))
(equal term1 (cdr temp-temp)))
(t (setq unify-subst (cons (cons term2 term1)
unify-subst))
t)))
((atom term1)
nil)
((eq (car term1)
(car term2))
(one-way-unify1-lst (cdr term1)
(cdr term2)))
(t nil)))
(defun one-way-unify1-lst (lst1 lst2)
(cond ((null lst1)
t)
((one-way-unify1 (car lst1)
(car lst2))
(one-way-unify1-lst (cdr lst1)
(cdr lst2)))
(t nil)))
(defun rewrite (term)
(cond ((atom term)
term)
(t (rewrite-with-lemmas (cons (car term)
(rewrite-args (cdr term)))
(get (car term)
(quote lemmas))))))
(defun rewrite-args (lst)
(cond ((null lst)
nil)
(t (cons (rewrite (car lst))
(rewrite-args (cdr lst))))))
(defun rewrite-with-lemmas (term lst)
(cond ((null lst)
term)
((one-way-unify term (cadr (car lst)))
(rewrite (apply-subst unify-subst (caddr (car lst)))))
(t (rewrite-with-lemmas term (cdr lst)))))
(defun
setup nil
(add-lemma-lst
(quote ((equal (compile form)
(reverse (codegen (optimize form)
(nil))))
(equal (eqp x y)
(equal (fix x)
(fix y)))
(equal (greaterp x y)
(lessp y x))
(equal (lesseqp x y)
(not (lessp y x)))
(equal (greatereqp x y)
(not (lessp x y)))
(equal (boolean x)
(or (equal x (t))
(equal x (f))))
(equal (iff x y)
(and (implies x y)
(implies y x)))
(equal (even1 x)
(if (zerop x)
(t)
(odd (sub1 x))))
(equal (countps- l pred)
(countps-loop l pred (zero)))
(equal (fact- i)
(fact-loop i 1))
(equal (reverse- x)
(reverse-loop x (nil)))
(equal (divides x y)
(zerop (remainder y x)))
(equal (assume-true var alist)
(cons (cons var (t))
alist))
(equal (assume-false var alist)
(cons (cons var (f))
alist))
(equal (tautology-checker x)
(tautologyp (normalize x)
(nil)))
(equal (falsify x)
(falsify1 (normalize x)
(nil)))
(equal (prime x)
(and (not (zerop x))
(not (equal x (add1 (zero))))
(prime1 x (sub1 x))))
(equal (and p q)
(if p (if q (t)
(f))
(f)))
(equal (or p q)
(if p (t)
(if q (t)
(f))
(f)))
(equal (not p)
(if p (f)
(t)))
(equal (implies p q)
(if p (if q (t)
(f))
(t)))
(equal (fix x)
(if (numberp x)
x
(zero)))
(equal (if (if a b c)
d e)
(if a (if b d e)
(if c d e)))
(equal (zerop x)
(or (equal x (zero))
(not (numberp x))))
(equal (plus (plus x y)
z)
(plus x (plus y z)))
(equal (equal (plus a b)
(zero))
(and (zerop a)
(zerop b)))
(equal (difference x x)
(zero))
(equal (equal (plus a b)
(plus a c))
(equal (fix b)
(fix c)))
(equal (equal (zero)
(difference x y))
(not (lessp y x)))
(equal (equal x (difference x y))
(and (numberp x)
(or (equal x (zero))
(zerop y))))
(equal (meaning (plus-tree (append x y))
a)
(plus (meaning (plus-tree x)
a)
(meaning (plus-tree y)
a)))
(equal (meaning (plus-tree (plus-fringe x))
a)
(fix (meaning x a)))
(equal (append (append x y)
z)
(append x (append y z)))
(equal (reverse (append a b))
(append (reverse b)
(reverse a)))
(equal (times x (plus y z))
(plus (times x y)
(times x z)))
(equal (times (times x y)
z)
(times x (times y z)))
(equal (equal (times x y)
(zero))
(or (zerop x)
(zerop y)))
(equal (exec (append x y)
pds envrn)
(exec y (exec x pds envrn)
envrn))
(equal (mc-flatten x y)
(append (flatten x)
y))
(equal (member x (append a b))
(or (member x a)
(member x b)))
(equal (member x (reverse y))
(member x y))
(equal (length (reverse x))
(length x))
(equal (member a (intersect b c))
(and (member a b)
(member a c)))
(equal (nth (zero)
i)
(zero))
(equal (exp i (plus j k))
(times (exp i j)
(exp i k)))
(equal (exp i (times j k))
(exp (exp i j)
k))
(equal (reverse-loop x y)
(append (reverse x)
y))
(equal (reverse-loop x (nil))
(reverse x))
(equal (count-list z (sort-lp x y))
(plus (count-list z x)
(count-list z y)))
(equal (equal (append a b)
(append a c))
(equal b c))
(equal (plus (remainder x y)
(times y (quotient x y)))
(fix x))
(equal (power-eval (big-plus1 l i base)
base)
(plus (power-eval l base)
i))
(equal (power-eval (big-plus x y i base)
base)
(plus i (plus (power-eval x base)
(power-eval y base))))
(equal (remainder y 1)
(zero))
(equal (lessp (remainder x y)
y)
(not (zerop y)))
(equal (remainder x x)
(zero))
(equal (lessp (quotient i j)
i)
(and (not (zerop i))
(or (zerop j)
(not (equal j 1)))))
(equal (lessp (remainder x y)
x)
(and (not (zerop y))
(not (zerop x))
(not (lessp x y))))
(equal (power-eval (power-rep i base)
base)
(fix i))
(equal (power-eval (big-plus (power-rep i base)
(power-rep j base)
(zero)
base)
base)
(plus i j))
(equal (gcd x y)
(gcd y x))
(equal (nth (append a b)
i)
(append (nth a i)
(nth b (difference i (length a)))))
(equal (difference (plus x y)
x)
(fix y))
(equal (difference (plus y x)
x)
(fix y))
(equal (difference (plus x y)
(plus x z))
(difference y z))
(equal (times x (difference c w))
(difference (times c x)
(times w x)))
(equal (remainder (times x z)
z)
(zero))
(equal (difference (plus b (plus a c))
a)
(plus b c))
(equal (difference (add1 (plus y z))
z)
(add1 y))
(equal (lessp (plus x y)
(plus x z))
(lessp y z))
(equal (lessp (times x z)
(times y z))
(and (not (zerop z))
(lessp x y)))
(equal (lessp y (plus x y))
(not (zerop x)))
(equal (gcd (times x z)
(times y z))
(times z (gcd x y)))
(equal (value (normalize x)
a)
(value x a))
(equal (equal (flatten x)
(cons y (nil)))
(and (nlistp x)
(equal x y)))
(equal (listp (gopher x))
(listp x))
(equal (samefringe x y)
(equal (flatten x)
(flatten y)))
(equal (equal (greatest-factor x y)
(zero))
(and (or (zerop y)
(equal y 1))
(equal x (zero))))
(equal (equal (greatest-factor x y)
1)
(equal x 1))
(equal (numberp (greatest-factor x y))
(not (and (or (zerop y)
(equal y 1))
(not (numberp x)))))
(equal (times-list (append x y))
(times (times-list x)
(times-list y)))
(equal (prime-list (append x y))
(and (prime-list x)
(prime-list y)))
(equal (equal z (times w z))
(and (numberp z)
(or (equal z (zero))
(equal w 1))))
(equal (greatereqpr x y)
(not (lessp x y)))
(equal (equal x (times x y))
(or (equal x (zero))
(and (numberp x)
(equal y 1))))
(equal (remainder (times y x)
y)
(zero))
(equal (equal (times a b)
1)
(and (not (equal a (zero)))
(not (equal b (zero)))
(numberp a)
(numberp b)
(equal (sub1 a)
(zero))
(equal (sub1 b)
(zero))))
(equal (lessp (length (delete x l))
(length l))
(member x l))
(equal (sort2 (delete x l))
(delete x (sort2 l)))
(equal (dsort x)
(sort2 x))
(equal (length (cons x1
(cons x2
(cons x3 (cons x4
(cons x5
(cons x6 x7)))))))
(plus 6 (length x7)))
(equal (difference (add1 (add1 x))
2)
(fix x))
(equal (quotient (plus x (plus x y))
2)
(plus x (quotient y 2)))
(equal (sigma (zero)
i)
(quotient (times i (add1 i))
2))
(equal (plus x (add1 y))
(if (numberp y)
(add1 (plus x y))
(add1 x)))
(equal (equal (difference x y)
(difference z y))
(if (lessp x y)
(not (lessp y z))
(if (lessp z y)
(not (lessp y x))
(equal (fix x)
(fix z)))))
(equal (meaning (plus-tree (delete x y))
a)
(if (member x y)
(difference (meaning (plus-tree y)
a)
(meaning x a))
(meaning (plus-tree y)
a)))
(equal (times x (add1 y))
(if (numberp y)
(plus x (times x y))
(fix x)))
(equal (nth (nil)
i)
(if (zerop i)
(nil)
(zero)))
(equal (last (append a b))
(if (listp b)
(last b)
(if (listp a)
(cons (car (last a))
b)
b)))
(equal (equal (lessp x y)
z)
(if (lessp x y)
(equal t z)
(equal f z)))
(equal (assignment x (append a b))
(if (assignedp x a)
(assignment x a)
(assignment x b)))
(equal (car (gopher x))
(if (listp x)
(car (flatten x))
(zero)))
(equal (flatten (cdr (gopher x)))
(if (listp x)
(cdr (flatten x))
(cons (zero)
(nil))))
(equal (quotient (times y x)
y)
(if (zerop y)
(zero)
(fix x)))
(equal (get j (set i val mem))
(if (eqp j i)
val
(get j mem)))))))
(defun tautologyp (x true-lst false-lst)
(cond ((truep x true-lst)
t)
((falsep x false-lst)
nil)
((atom x)
nil)
((eq (car x)
(quote if))
(cond ((truep (cadr x)
true-lst)
(tautologyp (caddr x)
true-lst false-lst))
((falsep (cadr x)
false-lst)
(tautologyp (cadddr x)
true-lst false-lst))
(t (and (tautologyp (caddr x)
(cons (cadr x)
true-lst)
false-lst)
(tautologyp (cadddr x)
true-lst
(cons (cadr x)
false-lst))))))
(t nil)))
(defun tautp (x)
(tautologyp (rewrite x)
nil nil))
(defun test nil
(prog (tm1 tm2 ans term)
(setq tm1 (ptime))
(setq term
(apply-subst
(quote ((x f (plus (plus a b)
(plus c (zero))))
(y f (times (times a b)
(plus c d)))
(z f (reverse (append (append a b)
(nil))))
(u equal (plus a b)
(difference x y))
(w lessp (remainder a b)
(member a (length b)))))
(quote (implies (and (implies x y)
(and (implies y z)
(and (implies z u)
(implies u w))))
(implies x w)))))
(setq ans (tautp term))
(setq tm2 (ptime))
(return (list ans (difference (car tm2)
(car tm1))
(difference (cadr tm2)
(cadr tm1))))))
(defun trans-of-implies (n)
(list (quote implies)
(trans-of-implies1 n)
(list (quote implies)
0 n)))
(defun trans-of-implies1 (n)
(cond ((equal n 1)
(list (quote implies)
0 1))
(t (list (quote and)
(list (quote implies)
(sub1 n)
n)
(trans-of-implies1 (sub1 n))))))
(defun truep (x lst)
(or (equal x (quote (t)))
(member x lst)))
The ELISP code
(DECLARE (SPECIAL UNIFY-SUBST TEMP-TEMP))
(DE ADD-LEMMA (TERM)
(COND ((AND (NOT (ATOM TERM))
(EQ (CAR TERM)
(QUOTE EQUAL))
(NOT (ATOM (CADR TERM))))
(PUTPROP (CAR (CADR TERM))
(CONS TERM (GET (CAR (CADR TERM))
(QUOTE LEMMAS)))
(QUOTE LEMMAS)))
(T (ERROR (LIST (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM) TERM)
))))
(DE ADD-LEMMA-LST (LST)
(COND ((NULL LST)
T)
(T (ADD-LEMMA (CAR LST))
(ADD-LEMMA-LST (CDR LST)))))
(DE APPLY-SUBST (ALIST TERM)
(COND ((ATOM TERM)
(COND ((SETQ TEMP-TEMP (ASSOC TERM ALIST))
(CDR TEMP-TEMP))
(T TERM)))
(T (CONS (CAR TERM)
(APPLY-SUBST-LST ALIST (CDR TERM))))))
(DE APPLY-SUBST-LST (ALIST LST)
(COND ((NULL LST)
NIL)
(T (CONS (APPLY-SUBST ALIST (CAR LST))
(APPLY-SUBST-LST ALIST (CDR LST))))))
(DE FALSEP (X LST)
(OR (EQUAL X (QUOTE (F)))
(MEMBER X LST)))
(DE ONE-WAY-UNIFY (TERM1 TERM2)
(PROGN (SETQ UNIFY-SUBST NIL)
(ONE-WAY-UNIFY1 TERM1 TERM2)))
(DE ONE-WAY-UNIFY1 (TERM1 TERM2)
(COND ((ATOM TERM2)
(COND ((SETQ TEMP-TEMP (ASSOC TERM2 UNIFY-SUBST))
(EQUAL TERM1 (CDR TEMP-TEMP)))
(T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
UNIFY-SUBST))
T)))
((ATOM TERM1)
NIL)
((EQ (CAR TERM1)
(CAR TERM2))
(ONE-WAY-UNIFY1-LST (CDR TERM1)
(CDR TERM2)))
(T NIL)))
(DE ONE-WAY-UNIFY1-LST (LST1 LST2)
(COND ((NULL LST1)
T)
((ONE-WAY-UNIFY1 (CAR LST1)
(CAR LST2))
(ONE-WAY-UNIFY1-LST (CDR LST1)
(CDR LST2)))
(T NIL)))
(DE REWRITE (TERM)
(COND ((ATOM TERM)
TERM)
(T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
(REWRITE-ARGS (CDR TERM)))
(GET (CAR TERM)
(QUOTE LEMMAS))))))
(DE REWRITE-ARGS (LST)
(COND ((NULL LST)
NIL)
(T (CONS (REWRITE (CAR LST))
(REWRITE-ARGS (CDR LST))))))
(DE REWRITE-WITH-LEMMAS (TERM LST)
(COND ((NULL LST)
TERM)
((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
(REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
(T (REWRITE-WITH-LEMMAS TERM (CDR LST)))))
(DE
SETUP NIL
(ADD-LEMMA-LST
(QUOTE ((EQUAL (COMPILE FORM)
(REVERSE (CODEGEN (OPTIMIZE FORM)
(NIL))))
(EQUAL (EQP X Y)
(EQUAL (FIX X)
(FIX Y)))
(EQUAL (GREATERP X Y)
(LESSP Y X))
(EQUAL (LESSEQP X Y)
(NOT (LESSP Y X)))
(EQUAL (GREATEREQP X Y)
(NOT (LESSP X Y)))
(EQUAL (BOOLEAN X)
(OR (EQUAL X (T))
(EQUAL X (F))))
(EQUAL (IFF X Y)
(AND (IMPLIES X Y)
(IMPLIES Y X)))
(EQUAL (EVEN1 X)
(IF (ZEROP X)
(T)
(ODD (SUB1 X))))
(EQUAL (COUNTPS- L PRED)
(COUNTPS-LOOP L PRED (ZERO)))
(EQUAL (FACT- I)
(FACT-LOOP I 1))
(EQUAL (REVERSE- X)
(REVERSE-LOOP X (NIL)))
(EQUAL (DIVIDES X Y)
(ZEROP (REMAINDER Y X)))
(EQUAL (ASSUME-TRUE VAR ALIST)
(CONS (CONS VAR (T))
ALIST))
(EQUAL (ASSUME-FALSE VAR ALIST)
(CONS (CONS VAR (F))
ALIST))
(EQUAL (TAUTOLOGY-CHECKER X)
(TAUTOLOGYP (NORMALIZE X)
(NIL)))
(EQUAL (FALSIFY X)
(FALSIFY1 (NORMALIZE X)
(NIL)))
(EQUAL (PRIME X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X (ADD1 (ZERO))))
(PRIME1 X (SUB1 X))))
(EQUAL (AND P Q)
(IF P (IF Q (T)
(F))
(F)))
(EQUAL (OR P Q)
(IF P (T)
(IF Q (T)
(F))
(F)))
(EQUAL (NOT P)
(IF P (F)
(T)))
(EQUAL (IMPLIES P Q)
(IF P (IF Q (T)
(F))
(T)))
(EQUAL (FIX X)
(IF (NUMBERP X)
X
(ZERO)))
(EQUAL (IF (IF A B C)
D E)
(IF A (IF B D E)
(IF C D E)))
(EQUAL (ZEROP X)
(OR (EQUAL X (ZERO))
(NOT (NUMBERP X))))
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z)))
(EQUAL (EQUAL (PLUS A B)
(ZERO))
(AND (ZEROP A)
(ZEROP B)))
(EQUAL (DIFFERENCE X X)
(ZERO))
(EQUAL (EQUAL (PLUS A B)
(PLUS A C))
(EQUAL (FIX B)
(FIX C)))
(EQUAL (EQUAL (ZERO)
(DIFFERENCE X Y))
(NOT (LESSP Y X)))
(EQUAL (EQUAL X (DIFFERENCE X Y))
(AND (NUMBERP X)
(OR (EQUAL X (ZERO))
(ZEROP Y))))
(EQUAL (MEANING (PLUS-TREE (APPEND X Y))
A)
(PLUS (MEANING (PLUS-TREE X)
A)
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
A)
(FIX (MEANING X A)))
(EQUAL (APPEND (APPEND X Y)
Z)
(APPEND X (APPEND Y Z)))
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B)
(REVERSE A)))
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z)))
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z)))
(EQUAL (EQUAL (TIMES X Y)
(ZERO))
(OR (ZEROP X)
(ZEROP Y)))
(EQUAL (EXEC (APPEND X Y)
PDS ENVRN)
(EXEC Y (EXEC X PDS ENVRN)
ENVRN))
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X)
Y))
(EQUAL (MEMBER X (APPEND A B))
(OR (MEMBER X A)
(MEMBER X B)))
(EQUAL (MEMBER X (REVERSE Y))
(MEMBER X Y))
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))
(EQUAL (MEMBER A (INTERSECT B C))
(AND (MEMBER A B)
(MEMBER A C)))
(EQUAL (NTH (ZERO)
I)
(ZERO))
(EQUAL (EXP I (PLUS J K))
(TIMES (EXP I J)
(EXP I K)))
(EQUAL (EXP I (TIMES J K))
(EXP (EXP I J)
K))
(EQUAL (REVERSE-LOOP X Y)
(APPEND (REVERSE X)
Y))
(EQUAL (REVERSE-LOOP X (NIL))
(REVERSE X))
(EQUAL (COUNT-LIST Z (SORT-LP X Y))
(PLUS (COUNT-LIST Z X)
(COUNT-LIST Z Y)))
(EQUAL (EQUAL (APPEND A B)
(APPEND A C))
(EQUAL B C))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
(FIX X))
(EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
BASE)
(PLUS (POWER-EVAL L BASE)
I))
(EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
BASE)
(PLUS I (PLUS (POWER-EVAL X BASE)
(POWER-EVAL Y BASE))))
(EQUAL (REMAINDER Y 1)
(ZERO))
(EQUAL (LESSP (REMAINDER X Y)
Y)
(NOT (ZEROP Y)))
(EQUAL (REMAINDER X X)
(ZERO))
(EQUAL (LESSP (QUOTIENT I J)
I)
(AND (NOT (ZEROP I))
(OR (ZEROP J)
(NOT (EQUAL J 1)))))
(EQUAL (LESSP (REMAINDER X Y)
X)
(AND (NOT (ZEROP Y))
(NOT (ZEROP X))
(NOT (LESSP X Y))))
(EQUAL (POWER-EVAL (POWER-REP I BASE)
BASE)
(FIX I))
(EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
(POWER-REP J BASE)
(ZERO)
BASE)
BASE)
(PLUS I J))
(EQUAL (GCD X Y)
(GCD Y X))
(EQUAL (NTH (APPEND A B)
I)
(APPEND (NTH A I)
(NTH B (DIFFERENCE I (LENGTH A)))))
(EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS X Y)
(PLUS X Z))
(DIFFERENCE Y Z))
(EQUAL (TIMES X (DIFFERENCE C W))
(DIFFERENCE (TIMES C X)
(TIMES W X)))
(EQUAL (REMAINDER (TIMES X Z)
Z)
(ZERO))
(EQUAL (DIFFERENCE (PLUS B (PLUS A C))
A)
(PLUS B C))
(EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
Z)
(ADD1 Y))
(EQUAL (LESSP (PLUS X Y)
(PLUS X Z))
(LESSP Y Z))
(EQUAL (LESSP (TIMES X Z)
(TIMES Y Z))
(AND (NOT (ZEROP Z))
(LESSP X Y)))
(EQUAL (LESSP Y (PLUS X Y))
(NOT (ZEROP X)))
(EQUAL (GCD (TIMES X Z)
(TIMES Y Z))
(TIMES Z (GCD X Y)))
(EQUAL (VALUE (NORMALIZE X)
A)
(VALUE X A))
(EQUAL (EQUAL (FLATTEN X)
(CONS Y (NIL)))
(AND (NLISTP X)
(EQUAL X Y)))
(EQUAL (LISTP (GOPHER X))
(LISTP X))
(EQUAL (SAMEFRINGE X Y)
(EQUAL (FLATTEN X)
(FLATTEN Y)))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
(ZERO))
(AND (OR (ZEROP Y)
(EQUAL Y 1))
(EQUAL X (ZERO))))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
1)
(EQUAL X 1))
(EQUAL (NUMBERP (GREATEST-FACTOR X Y))
(NOT (AND (OR (ZEROP Y)
(EQUAL Y 1))
(NOT (NUMBERP X)))))
(EQUAL (TIMES-LIST (APPEND X Y))
(TIMES (TIMES-LIST X)
(TIMES-LIST Y)))
(EQUAL (PRIME-LIST (APPEND X Y))
(AND (PRIME-LIST X)
(PRIME-LIST Y)))
(EQUAL (EQUAL Z (TIMES W Z))
(AND (NUMBERP Z)
(OR (EQUAL Z (ZERO))
(EQUAL W 1))))
(EQUAL (GREATEREQPR X Y)
(NOT (LESSP X Y)))
(EQUAL (EQUAL X (TIMES X Y))
(OR (EQUAL X (ZERO))
(AND (NUMBERP X)
(EQUAL Y 1))))
(EQUAL (REMAINDER (TIMES Y X)
Y)
(ZERO))
(EQUAL (EQUAL (TIMES A B)
1)
(AND (NOT (EQUAL A (ZERO)))
(NOT (EQUAL B (ZERO)))
(NUMBERP A)
(NUMBERP B)
(EQUAL (SUB1 A)
(ZERO))
(EQUAL (SUB1 B)
(ZERO))))
(EQUAL (LESSP (LENGTH (DELETE X L))
(LENGTH L))
(MEMBER X L))
(EQUAL (SORT2 (DELETE X L))
(DELETE X (SORT2 L)))
(EQUAL (DSORT X)
(SORT2 X))
(EQUAL (LENGTH (CONS X1
(CONS X2
(CONS X3 (CONS X4
(CONS X5
(CONS X6 X7)))))))
(PLUS 6 (LENGTH X7)))
(EQUAL (DIFFERENCE (ADD1 (ADD1 X))
2)
(FIX X))
(EQUAL (QUOTIENT (PLUS X (PLUS X Y))
2)
(PLUS X (QUOTIENT Y 2)))
(EQUAL (SIGMA (ZERO)
I)
(QUOTIENT (TIMES I (ADD1 I))
2))
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))
(EQUAL (EQUAL (DIFFERENCE X Y)
(DIFFERENCE Z Y))
(IF (LESSP X Y)
(NOT (LESSP Y Z))
(IF (LESSP Z Y)
(NOT (LESSP Y X))
(EQUAL (FIX X)
(FIX Z)))))
(EQUAL (MEANING (PLUS-TREE (DELETE X Y))
A)
(IF (MEMBER X Y)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING X A))
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))
(EQUAL (NTH (NIL)
I)
(IF (ZEROP I)
(NIL)
(ZERO)))
(EQUAL (LAST (APPEND A B))
(IF (LISTP B)
(LAST B)
(IF (LISTP A)
(CONS (CAR (LAST A))
B)
B)))
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z)))
(EQUAL (ASSIGNMENT X (APPEND A B))
(IF (ASSIGNEDP X A)
(ASSIGNMENT X A)
(ASSIGNMENT X B)))
(EQUAL (CAR (GOPHER X))
(IF (LISTP X)
(CAR (FLATTEN X))
(ZERO)))
(EQUAL (FLATTEN (CDR (GOPHER X)))
(IF (LISTP X)
(CDR (FLATTEN X))
(CONS (ZERO)
(NIL))))
(EQUAL (QUOTIENT (TIMES Y X)
Y)
(IF (ZEROP Y)
(ZERO)
(FIX X)))
(EQUAL (GET J (SET I VAL MEM))
(IF (EQP J I)
VAL
(GET J MEM)))))))
(DE TAUTOLOGYP (X TRUE-LST FALSE-LST)
(COND ((TRUEP X TRUE-LST)
T)
((FALSEP X FALSE-LST)
NIL)
((ATOM X)
NIL)
((EQ (CAR X)
(QUOTE IF))
(COND ((TRUEP (CADR X)
TRUE-LST)
(TAUTOLOGYP (CADDR X)
TRUE-LST FALSE-LST))
((FALSEP (CADR X)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST FALSE-LST))
(T (AND (TAUTOLOGYP (CADDR X)
(CONS (CADR X)
TRUE-LST)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST
(CONS (CADR X)
FALSE-LST))))))
(T NIL)))
(DE TAUTP (X)
(TAUTOLOGYP (REWRITE X)
NIL NIL))
(DE TEST NIL
(TIMER (TEST1)))
(DE TEST1 NIL
(PROG (TERM ANS)
(SETQ TERM
(APPLY-SUBST
(QUOTE ((X F (PLUS (PLUS A B)
(PLUS C (ZERO))))
(Y F (TIMES (TIMES A B)
(PLUS C D)))
(Z F (REVERSE (APPEND (APPEND A B)
(NIL))))
(U EQUAL (PLUS A B)
(DIFFERENCE X Y))
(W LESSP (REMAINDER A B)
(MEMBER A (LENGTH B)))))
(QUOTE (IMPLIES (AND (IMPLIES X Y)
(AND (IMPLIES Y Z)
(AND (IMPLIES Z U)
(IMPLIES U W))))
(IMPLIES X W)))))
(SETQ ANS (TAUTP TERM))
(RETURN (LIST ANS))))
(DE TRANS-OF-IMPLIES (N)
(LIST (QUOTE IMPLIES)
(TRANS-OF-IMPLIES1 N)
(LIST (QUOTE IMPLIES)
0 N)))
(DE TRANS-OF-IMPLIES1 (N)
(COND ((EQUAL N 1)
(LIST (QUOTE IMPLIES)
0 1))
(T (LIST (QUOTE AND)
(LIST (QUOTE IMPLIES)
(SUB1 N)
N)
(TRANS-OF-IMPLIES1 (SUB1 N))))))
(DE TRUEP (X LST)
(OR (EQUAL X (QUOTE (T)))
(MEMBER X LST)))
(FILECREATED " 5-Jul-82 12:52:49" <CL.BOYER.LISPS>IREWRITE..4 14918
changes to: IREWRITECOMS
previous date: " 5-Jul-82 12:11:22" <CL.BOYER.LISPS>IREWRITE..3)
(PRETTYCOMPRINT IREWRITECOMS)
(RPAQQ IREWRITECOMS ((FNS * IREWRITEFNS)
(PROP BLKLIBRARYDEF MEMBER)
(BLOCKS (REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST
APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY
ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME
REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS
SETUP TAUTOLOGYP TAUTP TEST
TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP
(ENTRIES TEST SETUP)
(BLKLIBRARY EQUAL MEMBER GETPROP)
(GLOBALVARS TEMP-TEMP UNIFY-SUBST)))))
(RPAQQ IREWRITEFNS (ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST
FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1
ONE-WAY-UNIFY1-LST PTIME REWRITE
REWRITE-ARGS REWRITE-WITH-LEMMAS SETUP
TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES
TRANS-OF-IMPLIES1 TRUEP))
(DEFINEQ
(ADD-LEMMA
(LAMBDA (TERM)
(COND
((AND (NOT (ATOM TERM))
(EQ (CAR TERM)
(QUOTE EQUAL))
(NOT (ATOM (CADR TERM))))
(COND
((GETPROP (CAR (CADR TERM))
(QUOTE LEMMAS))
(PUTPROP (CAR (CADR TERM))
(QUOTE LEMMAS)
(CONS TERM (GETPROP (CAR (CADR TERM))
(QUOTE LEMMAS)))))
(T (SETPROPLIST (CAR (CADR TERM))
(CONS (QUOTE LEMMAS)
(CONS (LIST TERM)
(GETPROPLIST (CAR (CADR TERM))))))
)))
(T (ERROR (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM)
TERM)))))
(ADD-LEMMA-LST
(LAMBDA (LST)
(COND
((NULL LST)
T)
(T (ADD-LEMMA (CAR LST))
(ADD-LEMMA-LST (CDR LST))))))
(APPLY-SUBST
(LAMBDA (ALIST TERM)
(COND
((NLISTP TERM)
(COND
((SETQ TEMP-TEMP (FASSOC TERM ALIST))
(CDR TEMP-TEMP))
(T TERM)))
(T (CONS (CAR TERM)
(APPLY-SUBST-LST ALIST (CDR TERM)))))))
(APPLY-SUBST-LST
(LAMBDA (ALIST LST)
(COND
((NULL LST)
NIL)
(T (CONS (APPLY-SUBST ALIST (CAR LST))
(APPLY-SUBST-LST ALIST (CDR LST)))))))
(FALSEP
(LAMBDA (X LST)
(OR (EQUAL X (QUOTE (F)))
(MEMBER X LST))))
(ONE-WAY-UNIFY
(LAMBDA (TERM1 TERM2)
(PROGN (SETQ UNIFY-SUBST NIL)
(ONE-WAY-UNIFY1 TERM1 TERM2))))
(ONE-WAY-UNIFY1
(LAMBDA (TERM1 TERM2)
(COND
((NLISTP TERM2)
(COND
((SETQ TEMP-TEMP (FASSOC TERM2 UNIFY-SUBST))
(EQUAL TERM1 (CDR TEMP-TEMP)))
(T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
UNIFY-SUBST))
T)))
((ATOM TERM1)
NIL)
((EQ (CAR TERM1)
(CAR TERM2))
(ONE-WAY-UNIFY1-LST (CDR TERM1)
(CDR TERM2)))
(T NIL))))
(ONE-WAY-UNIFY1-LST
(LAMBDA (LST1 LST2)
(COND
((NULL LST1)
T)
((ONE-WAY-UNIFY1 (CAR LST1)
(CAR LST2))
(ONE-WAY-UNIFY1-LST (CDR LST1)
(CDR LST2)))
(T NIL))))
(PTIME
(LAMBDA NIL
(PROG (GCTM)
(SETQ GCTM (CLOCK 3))
(RETURN (CONS (IPLUS (CLOCK 2)
GCTM)
GCTM)))))
(REWRITE
(LAMBDA (TERM)
(COND
((NLISTP TERM)
TERM)
(T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
(REWRITE-ARGS (CDR TERM)))
(GETPROP (CAR TERM)
(QUOTE LEMMAS)))))))
(REWRITE-ARGS
(LAMBDA (LST)
(COND
((NULL LST)
NIL)
(T (CONS (REWRITE (CAR LST))
(REWRITE-ARGS (CDR LST)))))))
(REWRITE-WITH-LEMMAS
(LAMBDA (TERM LST)
(COND
((NULL LST)
TERM)
((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
(REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
(T (REWRITE-WITH-LEMMAS TERM (CDR LST))))))
(SETUP
(LAMBDA NIL
(ADD-LEMMA-LST
(QUOTE
((EQUAL (COMPILE FORM)
(REVERSE (CODEGEN (OPTIMIZE FORM)
(NIL))))
(EQUAL (EQP X Y)
(EQUAL (FIX X)
(FIX Y)))
(EQUAL (GREATERP X Y)
(LESSP Y X))
(EQUAL (LESSEQP X Y)
(NOT (LESSP Y X)))
(EQUAL (GREATEREQP X Y)
(NOT (LESSP X Y)))
(EQUAL (BOOLEAN X)
(OR (EQUAL X (T))
(EQUAL X (F))))
(EQUAL (IFF X Y)
(AND (IMPLIES X Y)
(IMPLIES Y X)))
(EQUAL (EVEN1 X)
(IF (ZEROP X)
(T)
(ODD (SUB1 X))))
(EQUAL (COUNTPS- L PRED)
(COUNTPS-LOOP L PRED (ZERO)))
(EQUAL (FACT- I)
(FACT-LOOP I 1))
(EQUAL (REVERSE- X)
(REVERSE-LOOP X (NIL)))
(EQUAL (DIVIDES X Y)
(ZEROP (REMAINDER Y X)))
(EQUAL (ASSUME-TRUE VAR ALIST)
(CONS (CONS VAR (T))
ALIST))
(EQUAL (ASSUME-FALSE VAR ALIST)
(CONS (CONS VAR (F))
ALIST))
(EQUAL (TAUTOLOGY-CHECKER X)
(TAUTOLOGYP (NORMALIZE X)
(NIL)))
(EQUAL (FALSIFY X)
(FALSIFY1 (NORMALIZE X)
(NIL)))
(EQUAL (PRIME X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X (ADD1 (ZERO))))
(PRIME1 X (SUB1 X))))
(EQUAL (AND P Q)
(IF P (IF Q (T)
(F))
(F)))
(EQUAL (OR P Q)
(IF P (T)
(IF Q (T)
(F))
(F)))
(EQUAL (NOT P)
(IF P (F)
(T)))
(EQUAL (IMPLIES P Q)
(IF P (IF Q (T)
(F))
(T)))
(EQUAL (FIX X)
(IF (NUMBERP X)
X
(ZERO)))
(EQUAL (IF (IF A B C)
D E)
(IF A (IF B D E)
(IF C D E)))
(EQUAL (ZEROP X)
(OR (EQUAL X (ZERO))
(NOT (NUMBERP X))))
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z)))
(EQUAL (EQUAL (PLUS A B)
(ZERO))
(AND (ZEROP A)
(ZEROP B)))
(EQUAL (DIFFERENCE X X)
(ZERO))
(EQUAL (EQUAL (PLUS A B)
(PLUS A C))
(EQUAL (FIX B)
(FIX C)))
(EQUAL (EQUAL (ZERO)
(DIFFERENCE X Y))
(NOT (LESSP Y X)))
(EQUAL (EQUAL X (DIFFERENCE X Y))
(AND (NUMBERP X)
(OR (EQUAL X (ZERO))
(ZEROP Y))))
(EQUAL (MEANING (PLUS-TREE (APPEND X Y))
A)
(PLUS (MEANING (PLUS-TREE X)
A)
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
A)
(FIX (MEANING X A)))
(EQUAL (APPEND (APPEND X Y)
Z)
(APPEND X (APPEND Y Z)))
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B)
(REVERSE A)))
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z)))
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z)))
(EQUAL (EQUAL (TIMES X Y)
(ZERO))
(OR (ZEROP X)
(ZEROP Y)))
(EQUAL (EXEC (APPEND X Y)
PDS ENVRN)
(EXEC Y (EXEC X PDS ENVRN)
ENVRN))
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X)
Y))
(EQUAL (MEMBER X (APPEND A B))
(OR (MEMBER X A)
(MEMBER X B)))
(EQUAL (MEMBER X (REVERSE Y))
(MEMBER X Y))
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))
(EQUAL (MEMBER A (INTERSECT B C))
(AND (MEMBER A B)
(MEMBER A C)))
(EQUAL (NTH (ZERO)
I)
(ZERO))
(EQUAL (EXP I (PLUS J K))
(TIMES (EXP I J)
(EXP I K)))
(EQUAL (EXP I (TIMES J K))
(EXP (EXP I J)
K))
(EQUAL (REVERSE-LOOP X Y)
(APPEND (REVERSE X)
Y))
(EQUAL (REVERSE-LOOP X (NIL))
(REVERSE X))
(EQUAL (COUNT-LIST Z (SORT-LP X Y))
(PLUS (COUNT-LIST Z X)
(COUNT-LIST Z Y)))
(EQUAL (EQUAL (APPEND A B)
(APPEND A C))
(EQUAL B C))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
(FIX X))
(EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
BASE)
(PLUS (POWER-EVAL L BASE)
I))
(EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
BASE)
(PLUS I (PLUS (POWER-EVAL X BASE)
(POWER-EVAL Y BASE))))
(EQUAL (REMAINDER Y 1)
(ZERO))
(EQUAL (LESSP (REMAINDER X Y)
Y)
(NOT (ZEROP Y)))
(EQUAL (REMAINDER X X)
(ZERO))
(EQUAL (LESSP (QUOTIENT I J)
I)
(AND (NOT (ZEROP I))
(OR (ZEROP J)
(NOT (EQUAL J 1)))))
(EQUAL (LESSP (REMAINDER X Y)
X)
(AND (NOT (ZEROP Y))
(NOT (ZEROP X))
(NOT (LESSP X Y))))
(EQUAL (POWER-EVAL (POWER-REP I BASE)
BASE)
(FIX I))
(EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
(POWER-REP J BASE)
(ZERO)
BASE)
BASE)
(PLUS I J))
(EQUAL (GCD X Y)
(GCD Y X))
(EQUAL (NTH (APPEND A B)
I)
(APPEND (NTH A I)
(NTH B (DIFFERENCE I (LENGTH A)))))
(EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS X Y)
(PLUS X Z))
(DIFFERENCE Y Z))
(EQUAL (TIMES X (DIFFERENCE C W))
(DIFFERENCE (TIMES C X)
(TIMES W X)))
(EQUAL (REMAINDER (TIMES X Z)
Z)
(ZERO))
(EQUAL (DIFFERENCE (PLUS B (PLUS A C))
A)
(PLUS B C))
(EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
Z)
(ADD1 Y))
(EQUAL (LESSP (PLUS X Y)
(PLUS X Z))
(LESSP Y Z))
(EQUAL (LESSP (TIMES X Z)
(TIMES Y Z))
(AND (NOT (ZEROP Z))
(LESSP X Y)))
(EQUAL (LESSP Y (PLUS X Y))
(NOT (ZEROP X)))
(EQUAL (GCD (TIMES X Z)
(TIMES Y Z))
(TIMES Z (GCD X Y)))
(EQUAL (VALUE (NORMALIZE X)
A)
(VALUE X A))
(EQUAL (EQUAL (FLATTEN X)
(CONS Y (NIL)))
(AND (NLISTP X)
(EQUAL X Y)))
(EQUAL (LISTP (GOPHER X))
(LISTP X))
(EQUAL (SAMEFRINGE X Y)
(EQUAL (FLATTEN X)
(FLATTEN Y)))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
(ZERO))
(AND (OR (ZEROP Y)
(EQUAL Y 1))
(EQUAL X (ZERO))))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
1)
(EQUAL X 1))
(EQUAL (NUMBERP (GREATEST-FACTOR X Y))
(NOT (AND (OR (ZEROP Y)
(EQUAL Y 1))
(NOT (NUMBERP X)))))
(EQUAL (TIMES-LIST (APPEND X Y))
(TIMES (TIMES-LIST X)
(TIMES-LIST Y)))
(EQUAL (PRIME-LIST (APPEND X Y))
(AND (PRIME-LIST X)
(PRIME-LIST Y)))
(EQUAL (EQUAL Z (TIMES W Z))
(AND (NUMBERP Z)
(OR (EQUAL Z (ZERO))
(EQUAL W 1))))
(EQUAL (GREATEREQPR X Y)
(NOT (LESSP X Y)))
(EQUAL (EQUAL X (TIMES X Y))
(OR (EQUAL X (ZERO))
(AND (NUMBERP X)
(EQUAL Y 1))))
(EQUAL (REMAINDER (TIMES Y X)
Y)
(ZERO))
(EQUAL (EQUAL (TIMES A B)
1)
(AND (NOT (EQUAL A (ZERO)))
(NOT (EQUAL B (ZERO)))
(NUMBERP A)
(NUMBERP B)
(EQUAL (SUB1 A)
(ZERO))
(EQUAL (SUB1 B)
(ZERO))))
(EQUAL (LESSP (LENGTH (DELETE X L))
(LENGTH L))
(MEMBER X L))
(EQUAL (SORT2 (DELETE X L))
(DELETE X (SORT2 L)))
(EQUAL (DSORT X)
(SORT2 X))
(EQUAL
(LENGTH (CONS X1
(CONS X2
(CONS X3
(CONS X4 (CONS X5
(CONS X6 X7)))))))
(PLUS 6 (LENGTH X7)))
(EQUAL (DIFFERENCE (ADD1 (ADD1 X))
2)
(FIX X))
(EQUAL (QUOTIENT (PLUS X (PLUS X Y))
2)
(PLUS X (QUOTIENT Y 2)))
(EQUAL (SIGMA (ZERO)
I)
(QUOTIENT (TIMES I (ADD1 I))
2))
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))
(EQUAL (EQUAL (DIFFERENCE X Y)
(DIFFERENCE Z Y))
(IF (LESSP X Y)
(NOT (LESSP Y Z))
(IF (LESSP Z Y)
(NOT (LESSP Y X))
(EQUAL (FIX X)
(FIX Z)))))
(EQUAL (MEANING (PLUS-TREE (DELETE X Y))
A)
(IF (MEMBER X Y)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING X A))
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))
(EQUAL (NTH (NIL)
I)
(IF (ZEROP I)
(NIL)
(ZERO)))
(EQUAL (LAST (APPEND A B))
(IF (LISTP B)
(LAST B)
(IF (LISTP A)
(CONS (CAR (LAST A))
B)
B)))
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z)))
(EQUAL (ASSIGNMENT X (APPEND A B))
(IF (ASSIGNEDP X A)
(ASSIGNMENT X A)
(ASSIGNMENT X B)))
(EQUAL (CAR (GOPHER X))
(IF (LISTP X)
(CAR (FLATTEN X))
(ZERO)))
(EQUAL (FLATTEN (CDR (GOPHER X)))
(IF (LISTP X)
(CDR (FLATTEN X))
(CONS (ZERO)
(NIL))))
(EQUAL (QUOTIENT (TIMES Y X)
Y)
(IF (ZEROP Y)
(ZERO)
(FIX X)))
(EQUAL (GET J (SET I VAL MEM))
(IF (EQP J I)
VAL
(GET J MEM))))))))
(TAUTOLOGYP
(LAMBDA (X TRUE-LST FALSE-LST)
(COND
((TRUEP X TRUE-LST)
T)
((FALSEP X FALSE-LST)
NIL)
((NLISTP X)
NIL)
((EQ (CAR X)
(QUOTE IF))
(COND
((TRUEP (CADR X)
TRUE-LST)
(TAUTOLOGYP (CADDR X)
TRUE-LST FALSE-LST))
((FALSEP (CADR X)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST FALSE-LST))
(T (AND (TAUTOLOGYP (CADDR X)
(CONS (CADR X)
TRUE-LST)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST
(CONS (CADR X)
FALSE-LST))))))
(T NIL))))
(TAUTP
(LAMBDA (X)
(TAUTOLOGYP (REWRITE X)
NIL NIL)))
(TEST
(LAMBDA NIL
(PROG (TM1 TM2 ANS TERM)
(SETQ TM1 (PTIME))
(SETQ TERM
(APPLY-SUBST
(QUOTE ((X F (PLUS (PLUS A B)
(PLUS C (ZERO))))
(Y F (TIMES (TIMES A B)
(PLUS C D)))
(Z F (REVERSE (APPEND (APPEND A B)
(NIL))))
(U EQUAL (PLUS A B)
(DIFFERENCE X Y))
(W LESSP (REMAINDER A B)
(MEMBER A (LENGTH B)))))
(QUOTE (IMPLIES (AND (IMPLIES X Y)
(AND (IMPLIES Y Z)
(AND (IMPLIES Z U)
(IMPLIES U W))))
(IMPLIES X W)))))
(SETQ ANS (TAUTP TERM))
(SETQ TM2 (PTIME))
(RETURN (LIST ANS (DIFFERENCE (CAR TM2)
(CAR TM1))
(DIFFERENCE (CDR TM2)
(CDR TM1)))))))
(TRANS-OF-IMPLIES
(LAMBDA (N)
(LIST (QUOTE IMPLIES)
(TRANS-OF-IMPLIES1 N)
(LIST (QUOTE IMPLIES)
0 N))))
(TRANS-OF-IMPLIES1
(LAMBDA (N)
(COND
((EQUAL N 1)
(LIST (QUOTE IMPLIES)
0 1))
(T (LIST (QUOTE AND)
(LIST (QUOTE IMPLIES)
(SUB1 N)
N)
(TRANS-OF-IMPLIES1 (SUB1 N)))))))
(TRUEP
(LAMBDA (X LST)
(OR (EQUAL X (QUOTE (T)))
(MEMBER X LST))))
)
(PUTPROPS MEMBER BLKLIBRARYDEF (LAMBDA
(.BLKVAR.X .BLKVAR.Y)
(DECLARE (LOCALVARS . T))
(PROG NIL LP (RETURN (COND ((NLISTP .BLKVAR.Y)
NIL)
((EQUAL .BLKVAR.X (CAR .BLKVAR.Y)
)
.BLKVAR.Y)
(T (SETQ .BLKVAR.Y (CDR
.BLKVAR.Y))
(GO LP)))))))
[DECLARE: DONTEVAL@LOAD DOEVAL@COMPILE DONTCOPY
(BLOCK: REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST
APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY ONE-WAY-UNIFY1
ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS
REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST
TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES TEST SETUP)
(BLKLIBRARY EQUAL MEMBER GETPROP)
(GLOBALVARS TEMP-TEMP UNIFY-SUBST))
]
(DECLARE: DONTCOPY
(FILEMAP (NIL (1018 14165 (ADD-LEMMA 1030 . 1573) (ADD-LEMMA-LST 1577 .
1708) (APPLY-SUBST 1712 . 1945) (APPLY-SUBST-LST 1949 . 2119) (FALSEP
2123 . 2200) (ONE-WAY-UNIFY 2204 . 2315) (ONE-WAY-UNIFY1 2319 . 2717) (
ONE-WAY-UNIFY1-LST 2721 . 2928) (PTIME 2932 . 3077) (REWRITE 3081 . 3295
) (REWRITE-ARGS 3299 . 3441) (REWRITE-WITH-LEMMAS 3445 . 3679) (SETUP
3683 . 12295) (TAUTOLOGYP 12299 . 12890) (TAUTP 12894 . 12958) (TEST
12962 . 13720) (TRANS-OF-IMPLIES 13724 . 13846) (TRANS-OF-IMPLIES1 13850
. 14082) (TRUEP 14086 . 14162)))))
STOP
The Maclisp Code
(DECLARE (SPECIAL UNIFY-SUBST TEMP-TEMP))
(DEFUN PTIME NIL (LIST (RUNTIME) (STATUS GCTIME)))
(DEFUN ADD-LEMMA (TERM)
(COND ((AND (NOT (ATOM TERM))
(EQ (CAR TERM)
(QUOTE EQUAL))
(NOT (ATOM (CADR TERM))))
(PUTPROP (CAR (CADR TERM))
(CONS TERM (GET (CAR (CADR TERM))
(QUOTE LEMMAS)))
(QUOTE LEMMAS)))
(T (ERROR (QUOTE ADD-LEMMA-DID-NOT-LIKE-TERM)
TERM))))
(DEFUN ADD-LEMMA-LST (LST)
(COND ((NULL LST)
T)
(T (ADD-LEMMA (CAR LST))
(ADD-LEMMA-LST (CDR LST)))))
(DEFUN APPLY-SUBST (ALIST TERM)
(COND ((ATOM TERM)
(COND ((SETQ TEMP-TEMP (ASSQ TERM ALIST))
(CDR TEMP-TEMP))
(T TERM)))
(T (CONS (CAR TERM)
(APPLY-SUBST-LST ALIST (CDR TERM))))))
(DEFUN APPLY-SUBST-LST (ALIST LST)
(COND ((NULL LST)
NIL)
(T (CONS (APPLY-SUBST ALIST (CAR LST))
(APPLY-SUBST-LST ALIST (CDR LST))))))
(DEFUN FALSEP (X LST)
(OR (EQUAL X (QUOTE (F)))
(MEMBER X LST)))
(DEFUN ONE-WAY-UNIFY (TERM1 TERM2)
(PROGN (SETQ UNIFY-SUBST NIL)
(ONE-WAY-UNIFY1 TERM1 TERM2)))
(DEFUN ONE-WAY-UNIFY1 (TERM1 TERM2)
(COND ((ATOM TERM2)
(COND ((SETQ TEMP-TEMP (ASSQ TERM2 UNIFY-SUBST))
(EQUAL TERM1 (CDR TEMP-TEMP)))
(T (SETQ UNIFY-SUBST (CONS (CONS TERM2 TERM1)
UNIFY-SUBST))
T)))
((ATOM TERM1)
NIL)
((EQ (CAR TERM1)
(CAR TERM2))
(ONE-WAY-UNIFY1-LST (CDR TERM1)
(CDR TERM2)))
(T NIL)))
(DEFUN ONE-WAY-UNIFY1-LST (LST1 LST2)
(COND ((NULL LST1)
T)
((ONE-WAY-UNIFY1 (CAR LST1)
(CAR LST2))
(ONE-WAY-UNIFY1-LST (CDR LST1)
(CDR LST2)))
(T NIL)))
(DEFUN REWRITE (TERM)
(COND ((ATOM TERM)
TERM)
(T (REWRITE-WITH-LEMMAS (CONS (CAR TERM)
(REWRITE-ARGS (CDR TERM)))
(GET (CAR TERM)
(QUOTE LEMMAS))))))
(DEFUN REWRITE-ARGS (LST)
(COND ((NULL LST)
NIL)
(T (CONS (REWRITE (CAR LST))
(REWRITE-ARGS (CDR LST))))))
(DEFUN REWRITE-WITH-LEMMAS (TERM LST)
(COND ((NULL LST)
TERM)
((ONE-WAY-UNIFY TERM (CADR (CAR LST)))
(REWRITE (APPLY-SUBST UNIFY-SUBST (CADDR (CAR LST)))))
(T (REWRITE-WITH-LEMMAS TERM (CDR LST)))))
(DEFUN
SETUP NIL
(ADD-LEMMA-LST
(QUOTE ((EQUAL (COMPILE FORM)
(REVERSE (CODEGEN (OPTIMIZE FORM)
(NIL))))
(EQUAL (EQP X Y)
(EQUAL (FIX X)
(FIX Y)))
(EQUAL (GREATERP X Y)
(LESSP Y X))
(EQUAL (LESSEQP X Y)
(NOT (LESSP Y X)))
(EQUAL (GREATEREQP X Y)
(NOT (LESSP X Y)))
(EQUAL (BOOLEAN X)
(OR (EQUAL X (T))
(EQUAL X (F))))
(EQUAL (IFF X Y)
(AND (IMPLIES X Y)
(IMPLIES Y X)))
(EQUAL (EVEN1 X)
(IF (ZEROP X)
(T)
(ODD (SUB1 X))))
(EQUAL (COUNTPS- L PRED)
(COUNTPS-LOOP L PRED (ZERO)))
(EQUAL (FACT- I)
(FACT-LOOP I 1))
(EQUAL (REVERSE- X)
(REVERSE-LOOP X (NIL)))
(EQUAL (DIVIDES X Y)
(ZEROP (REMAINDER Y X)))
(EQUAL (ASSUME-TRUE VAR ALIST)
(CONS (CONS VAR (T))
ALIST))
(EQUAL (ASSUME-FALSE VAR ALIST)
(CONS (CONS VAR (F))
ALIST))
(EQUAL (TAUTOLOGY-CHECKER X)
(TAUTOLOGYP (NORMALIZE X)
(NIL)))
(EQUAL (FALSIFY X)
(FALSIFY1 (NORMALIZE X)
(NIL)))
(EQUAL (PRIME X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X (ADD1 (ZERO))))
(PRIME1 X (SUB1 X))))
(EQUAL (AND P Q)
(IF P (IF Q (T)
(F))
(F)))
(EQUAL (OR P Q)
(IF P (T)
(IF Q (T)
(F))
(F)))
(EQUAL (NOT P)
(IF P (F)
(T)))
(EQUAL (IMPLIES P Q)
(IF P (IF Q (T)
(F))
(T)))
(EQUAL (FIX X)
(IF (NUMBERP X)
X
(ZERO)))
(EQUAL (IF (IF A B C)
D E)
(IF A (IF B D E)
(IF C D E)))
(EQUAL (ZEROP X)
(OR (EQUAL X (ZERO))
(NOT (NUMBERP X))))
(EQUAL (PLUS (PLUS X Y)
Z)
(PLUS X (PLUS Y Z)))
(EQUAL (EQUAL (PLUS A B)
(ZERO))
(AND (ZEROP A)
(ZEROP B)))
(EQUAL (DIFFERENCE X X)
(ZERO))
(EQUAL (EQUAL (PLUS A B)
(PLUS A C))
(EQUAL (FIX B)
(FIX C)))
(EQUAL (EQUAL (ZERO)
(DIFFERENCE X Y))
(NOT (LESSP Y X)))
(EQUAL (EQUAL X (DIFFERENCE X Y))
(AND (NUMBERP X)
(OR (EQUAL X (ZERO))
(ZEROP Y))))
(EQUAL (MEANING (PLUS-TREE (APPEND X Y))
A)
(PLUS (MEANING (PLUS-TREE X)
A)
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
A)
(FIX (MEANING X A)))
(EQUAL (APPEND (APPEND X Y)
Z)
(APPEND X (APPEND Y Z)))
(EQUAL (REVERSE (APPEND A B))
(APPEND (REVERSE B)
(REVERSE A)))
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y)
(TIMES X Z)))
(EQUAL (TIMES (TIMES X Y)
Z)
(TIMES X (TIMES Y Z)))
(EQUAL (EQUAL (TIMES X Y)
(ZERO))
(OR (ZEROP X)
(ZEROP Y)))
(EQUAL (EXEC (APPEND X Y)
PDS ENVRN)
(EXEC Y (EXEC X PDS ENVRN)
ENVRN))
(EQUAL (MC-FLATTEN X Y)
(APPEND (FLATTEN X)
Y))
(EQUAL (MEMBER X (APPEND A B))
(OR (MEMBER X A)
(MEMBER X B)))
(EQUAL (MEMBER X (REVERSE Y))
(MEMBER X Y))
(EQUAL (LENGTH (REVERSE X))
(LENGTH X))
(EQUAL (MEMBER A (INTERSECT B C))
(AND (MEMBER A B)
(MEMBER A C)))
(EQUAL (NTH (ZERO)
I)
(ZERO))
(EQUAL (EXP I (PLUS J K))
(TIMES (EXP I J)
(EXP I K)))
(EQUAL (EXP I (TIMES J K))
(EXP (EXP I J)
K))
(EQUAL (REVERSE-LOOP X Y)
(APPEND (REVERSE X)
Y))
(EQUAL (REVERSE-LOOP X (NIL))
(REVERSE X))
(EQUAL (COUNT-LIST Z (SORT-LP X Y))
(PLUS (COUNT-LIST Z X)
(COUNT-LIST Z Y)))
(EQUAL (EQUAL (APPEND A B)
(APPEND A C))
(EQUAL B C))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
(FIX X))
(EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
BASE)
(PLUS (POWER-EVAL L BASE)
I))
(EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
BASE)
(PLUS I (PLUS (POWER-EVAL X BASE)
(POWER-EVAL Y BASE))))
(EQUAL (REMAINDER Y 1)
(ZERO))
(EQUAL (LESSP (REMAINDER X Y)
Y)
(NOT (ZEROP Y)))
(EQUAL (REMAINDER X X)
(ZERO))
(EQUAL (LESSP (QUOTIENT I J)
I)
(AND (NOT (ZEROP I))
(OR (ZEROP J)
(NOT (EQUAL J 1)))))
(EQUAL (LESSP (REMAINDER X Y)
X)
(AND (NOT (ZEROP Y))
(NOT (ZEROP X))
(NOT (LESSP X Y))))
(EQUAL (POWER-EVAL (POWER-REP I BASE)
BASE)
(FIX I))
(EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
(POWER-REP J BASE)
(ZERO)
BASE)
BASE)
(PLUS I J))
(EQUAL (GCD X Y)
(GCD Y X))
(EQUAL (NTH (APPEND A B)
I)
(APPEND (NTH A I)
(NTH B (DIFFERENCE I (LENGTH A)))))
(EQUAL (DIFFERENCE (PLUS X Y)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS Y X)
X)
(FIX Y))
(EQUAL (DIFFERENCE (PLUS X Y)
(PLUS X Z))
(DIFFERENCE Y Z))
(EQUAL (TIMES X (DIFFERENCE C W))
(DIFFERENCE (TIMES C X)
(TIMES W X)))
(EQUAL (REMAINDER (TIMES X Z)
Z)
(ZERO))
(EQUAL (DIFFERENCE (PLUS B (PLUS A C))
A)
(PLUS B C))
(EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
Z)
(ADD1 Y))
(EQUAL (LESSP (PLUS X Y)
(PLUS X Z))
(LESSP Y Z))
(EQUAL (LESSP (TIMES X Z)
(TIMES Y Z))
(AND (NOT (ZEROP Z))
(LESSP X Y)))
(EQUAL (LESSP Y (PLUS X Y))
(NOT (ZEROP X)))
(EQUAL (GCD (TIMES X Z)
(TIMES Y Z))
(TIMES Z (GCD X Y)))
(EQUAL (VALUE (NORMALIZE X)
A)
(VALUE X A))
(EQUAL (EQUAL (FLATTEN X)
(CONS Y (NIL)))
(AND (NLISTP X)
(EQUAL X Y)))
(EQUAL (LISTP (GOPHER X))
(LISTP X))
(EQUAL (SAMEFRINGE X Y)
(EQUAL (FLATTEN X)
(FLATTEN Y)))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
(ZERO))
(AND (OR (ZEROP Y)
(EQUAL Y 1))
(EQUAL X (ZERO))))
(EQUAL (EQUAL (GREATEST-FACTOR X Y)
1)
(EQUAL X 1))
(EQUAL (NUMBERP (GREATEST-FACTOR X Y))
(NOT (AND (OR (ZEROP Y)
(EQUAL Y 1))
(NOT (NUMBERP X)))))
(EQUAL (TIMES-LIST (APPEND X Y))
(TIMES (TIMES-LIST X)
(TIMES-LIST Y)))
(EQUAL (PRIME-LIST (APPEND X Y))
(AND (PRIME-LIST X)
(PRIME-LIST Y)))
(EQUAL (EQUAL Z (TIMES W Z))
(AND (NUMBERP Z)
(OR (EQUAL Z (ZERO))
(EQUAL W 1))))
(EQUAL (GREATEREQPR X Y)
(NOT (LESSP X Y)))
(EQUAL (EQUAL X (TIMES X Y))
(OR (EQUAL X (ZERO))
(AND (NUMBERP X)
(EQUAL Y 1))))
(EQUAL (REMAINDER (TIMES Y X)
Y)
(ZERO))
(EQUAL (EQUAL (TIMES A B)
1)
(AND (NOT (EQUAL A (ZERO)))
(NOT (EQUAL B (ZERO)))
(NUMBERP A)
(NUMBERP B)
(EQUAL (SUB1 A)
(ZERO))
(EQUAL (SUB1 B)
(ZERO))))
(EQUAL (LESSP (LENGTH (DELETE X L))
(LENGTH L))
(MEMBER X L))
(EQUAL (SORT2 (DELETE X L))
(DELETE X (SORT2 L)))
(EQUAL (DSORT X)
(SORT2 X))
(EQUAL (LENGTH (CONS X1
(CONS X2
(CONS X3 (CONS X4
(CONS X5
(CONS X6 X7)))))))
(PLUS 6 (LENGTH X7)))
(EQUAL (DIFFERENCE (ADD1 (ADD1 X))
2)
(FIX X))
(EQUAL (QUOTIENT (PLUS X (PLUS X Y))
2)
(PLUS X (QUOTIENT Y 2)))
(EQUAL (SIGMA (ZERO)
I)
(QUOTIENT (TIMES I (ADD1 I))
2))
(EQUAL (PLUS X (ADD1 Y))
(IF (NUMBERP Y)
(ADD1 (PLUS X Y))
(ADD1 X)))
(EQUAL (EQUAL (DIFFERENCE X Y)
(DIFFERENCE Z Y))
(IF (LESSP X Y)
(NOT (LESSP Y Z))
(IF (LESSP Z Y)
(NOT (LESSP Y X))
(EQUAL (FIX X)
(FIX Z)))))
(EQUAL (MEANING (PLUS-TREE (DELETE X Y))
A)
(IF (MEMBER X Y)
(DIFFERENCE (MEANING (PLUS-TREE Y)
A)
(MEANING X A))
(MEANING (PLUS-TREE Y)
A)))
(EQUAL (TIMES X (ADD1 Y))
(IF (NUMBERP Y)
(PLUS X (TIMES X Y))
(FIX X)))
(EQUAL (NTH (NIL)
I)
(IF (ZEROP I)
(NIL)
(ZERO)))
(EQUAL (LAST (APPEND A B))
(IF (LISTP B)
(LAST B)
(IF (LISTP A)
(CONS (CAR (LAST A))
B)
B)))
(EQUAL (EQUAL (LESSP X Y)
Z)
(IF (LESSP X Y)
(EQUAL T Z)
(EQUAL F Z)))
(EQUAL (ASSIGNMENT X (APPEND A B))
(IF (ASSIGNEDP X A)
(ASSIGNMENT X A)
(ASSIGNMENT X B)))
(EQUAL (CAR (GOPHER X))
(IF (LISTP X)
(CAR (FLATTEN X))
(ZERO)))
(EQUAL (FLATTEN (CDR (GOPHER X)))
(IF (LISTP X)
(CDR (FLATTEN X))
(CONS (ZERO)
(NIL))))
(EQUAL (QUOTIENT (TIMES Y X)
Y)
(IF (ZEROP Y)
(ZERO)
(FIX X)))
(EQUAL (GET J (SET I VAL MEM))
(IF (EQP J I)
VAL
(GET J MEM)))))))
(DEFUN TAUTOLOGYP (X TRUE-LST FALSE-LST)
(COND ((TRUEP X TRUE-LST)
T)
((FALSEP X FALSE-LST)
NIL)
((ATOM X)
NIL)
((EQ (CAR X)
(QUOTE IF))
(COND ((TRUEP (CADR X)
TRUE-LST)
(TAUTOLOGYP (CADDR X)
TRUE-LST FALSE-LST))
((FALSEP (CADR X)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST FALSE-LST))
(T (AND (TAUTOLOGYP (CADDR X)
(CONS (CADR X)
TRUE-LST)
FALSE-LST)
(TAUTOLOGYP (CADDDR X)
TRUE-LST
(CONS (CADR X)
FALSE-LST))))))
(T NIL)))
(DEFUN TAUTP (X)
(TAUTOLOGYP (REWRITE X)
NIL NIL))
(DEFUN TEST NIL
(PROG (TM1 TM2 ANS TERM)
(SETQ TM1 (PTIME))
(SETQ TERM
(APPLY-SUBST
(QUOTE ((X F (PLUS (PLUS A B)
(PLUS C (ZERO))))
(Y F (TIMES (TIMES A B)
(PLUS C D)))
(Z F (REVERSE (APPEND (APPEND A B)
(NIL))))
(U EQUAL (PLUS A B)
(DIFFERENCE X Y))
(W LESSP (REMAINDER A B)
(MEMBER A (LENGTH B)))))
(QUOTE (IMPLIES (AND (IMPLIES X Y)
(AND (IMPLIES Y Z)
(AND (IMPLIES Z U)
(IMPLIES U W))))
(IMPLIES X W)))))
(SETQ ANS (TAUTP TERM))
(SETQ TM2 (PTIME))
(RETURN (LIST ANS (DIFFERENCE (CAR TM2)
(CAR TM1))
(DIFFERENCE (CADR TM2)
(CADR TM1))))))
(DEFUN TRANS-OF-IMPLIES (N)
(LIST (QUOTE IMPLIES)
(TRANS-OF-IMPLIES1 N)
(LIST (QUOTE IMPLIES)
0 N)))
(DEFUN TRANS-OF-IMPLIES1 (N)
(COND ((EQUAL N 1)
(LIST (QUOTE IMPLIES)
0 1))
(T (LIST (QUOTE AND)
(LIST (QUOTE IMPLIES)
(SUB1 N)
N)
(TRANS-OF-IMPLIES1 (SUB1 N))))))
(DEFUN TRUEP (X LST)
(OR (EQUAL X (QUOTE (T)))
(MEMBER X LST)))
The FRANZ tests
Mail-from: ARPANET site SU-SCORE rcvd at 26-Nov-82 1711-CST
Date: 26 Nov 1982 1507-PST
From: Gordon Novak <CSD.NOVAK at SU-SCORE>
Subject: Franz Benchmark
To: CL.BOYER at UTEXAS-20
cc: kim.fateman at UCB-C70
*** EOOH ***
Date: Friday, 26 November 1982 17:07-CST
From: Gordon Novak <CSD.NOVAK at SU-SCORE>
To: CL.BOYER
cc: kim.fateman at UCB-C70
Re: Franz Benchmark
Bob,
Here are my results running your benchmark on Franz Lisp, on a
lightly loaded VAX 11/780. The program is on
[SCORE]<CSD.NOVAK>IREWRITE.FRANZ .
It is identical to the Maclisp program, except that I made it
lower-case and deleted the definition of PTIME, which is a system
function in Franz. Raw times are in units of 1/60 second.
With translink=nil:
Real time Result
3:40 (t 12104 4342)
2:50 (t 8850 1111)
2:50 (t 8885 1132)
2:43 (t 9024 1164)
3:13 (t 8853 942)
Avg.: 8903 1087 (first one omitted)
148.38 18.12 seconds
total GC
With (sstatus translink on):
Real time total gc
2:05 (t 6459 4279)
1:08 (t 3290 1110)
1:12 (t 3312 1114)
1:26 (t 3386 1151)
1:10 (t 3104 906)
1:03 (t 3061 887)
1:20 (t 3166 920)
Avg: 3219.8 1014.7
53.67 16.91 seconds
total GC
(first run omitted from average)
Cheers, Gordon
Mail-from: ARPANET site UCB-C70 rcvd at 26-Nov-82 1735-CST
Date: 26-Nov-82 15:32:57-PST (Fri)
From: Kim.fateman@Berkeley
Subject: Re: Franz Benchmark
Message-Id: <8210262337.27332@UCBVAX.BERKELEY.ARPA>
Received: by UCBVAX.BERKELEY.ARPA (3.227 [10/22/82])
id A27328; 26-Nov-82 15:37:08-PST (Fri)
To: CL.BOYER@UTEXAS-20, CSD.NOVAK@SU-SCORE
Cc: fateman@Kim@SU-SCORE, jkf@Kim@SU-SCORE
*** EOOH ***
Date: 26-Nov-82 15:32:57-PST (Fri)
From: Kim.fateman at Berkeley
To: CL.BOYER, CSD.NOVAK at SU-SCORE
cc: fateman at Kim at SU-SCORE, jkf at Kim at SU-SCORE
Re: Franz Benchmark
Received: by UCBVAX.BERKELEY.ARPA (3.227 [10/22/82])
id A27328; 26-Nov-82 15: 37:08-PST (Fri)
I don't know exactly what the benchmark is, (I'm grabbing a copy at the
moment), but it is sometimes relevant to note the version of Franz
and the version of the compiler. Some newer versions seem to have
gotten a bit slower. Also, there is another option for speeding up
function calls, which is to do (declare (localf <functions...>))
which makes it impossible to trace the functions, however, and works
only for functions compiled "at the same time".
Mail-from: ARPANET site UCB-C70 rcvd at 26-Nov-82 1845-CST
Date: 26-Nov-82 16:42:50-PST (Fri)
From: Kim.fateman@Berkeley
Subject: Re: Franz Benchmark
Message-Id: <8210270047.28393@UCBVAX.BERKELEY.ARPA>
Received: by UCBVAX.BERKELEY.ARPA (3.227 [10/22/82])
id A28381; 26-Nov-82 16:47:22-PST (Fri)
To: CL.BOYER@UTEXAS-20, CSD.NOVAK@SU-SCORE, fateman@Kim@SU-SCORE
Cc: jkf@Kim@SU-SCORE
*** EOOH ***
Date: 26-Nov-82 16:42:50-PST (Fri)
From: Kim.fateman at Berkeley
To: CL.BOYER, CSD.NOVAK at SU-SCORE, fateman at Kim at SU-SCORE
cc: jkf at Kim at SU-SCORE
Re: Franz Benchmark
Received: by UCBVAX.BERKELEY.ARPA (3.227 [10/22/82])
id A28381; 26-Nov-82 16: 47:22-PST (Fri)
I put in local function declarations, and compared the before and after.
The result of (setup)(test) with the declarations seems to be
about 40% of the times without. Every function but setup and test
were declared localf's.
My times are somewhat slower, overall, than you got.
Mail-from: ARPANET site UCB-C70 rcvd at 27-Nov-82 2353-CST
Date: 27-Nov-82 21:51:04-PST (Sat)
From: Kim.fateman@Berkeley
Subject: best times for irewrite
Message-Id: <8210280546.8211@UCBVAX.BERKELEY.ARPA>
Received: by UCBVAX.BERKELEY.ARPA (3.227 [10/22/82])
id A08204; 27-Nov-82 21:46:21-PST (Sat)
To: csd.novak@su-score
Cc: cl.boyer@UTEXAS-20
*** EOOH ***
Date: 27-Nov-82 21:51:04-PST (Sat)
From: Kim.fateman at Berkeley
To: csd.novak at su-score
cc: cl.boyer
Re: best times for irewrite
Received: by UCBVAX.BERKELEY.ARPA (3.227 [10/22/82])
id A08204; 27-Nov-82 21: 46:21-PST (Sat)
I thought my numbers were slower than yours for non-localf stuff;
I have heard various explanations for why this might be; one was
that 4.1aBSD timing routines run differently... Anyway, I expect
that if you put localf into your file, you'll get it to run faster yet.
Though what it all means, I don't know, quite.
Mail-from: ARPANET site UCB-C70 rcvd at 27-Nov-82 2310-CST
Date: 27-Nov-82 21:07:46-PST (Sat)
From: Kim.fateman@Berkeley
Subject: my numbers for irewrite
Message-Id: <8210280503.7600@UCBVAX.BERKELEY.ARPA>
Received: by UCBVAX.BERKELEY.ARPA (3.227 [10/22/82])
id A07598; 27-Nov-82 21:03:07-PST (Sat)
To: cl.boyer@utexas-20
Cc: csd.novak@su-score, fateman@Kim@su-score
*** EOOH ***
Date: 27-Nov-82 21:07:46-PST (Sat)
From: Kim.fateman at Berkeley
To: cl.boyer
cc: csd.novak at su-score, fateman at Kim at su-score
Re: my numbers for irewrite
Received: by UCBVAX.BERKELEY.ARPA (3.227 [10/22/82])
id A07598; 27-Nov-82 21: 03:07-PST (Sat)
Script started on Sat Nov 27 20:35:04 1982
uptime
8:35pm up 3:45, 6 users, load average: 0.57, 0.82, 0.93
% lisp
Franz Lisp, Opus 38.41
-> (load 'oirewrite)
[fasl oirewrite.o]
t
-> '(this is the original with no localf declaration)
(this is the original with no localf declaration)
-> (setup)
t
-> (test)
(t 15366 6676)
-> (test)
(t 10473 1271)
-> (sstatus translink on)
on
-> (test)
(t 3734 1290)
-> (test)
(t 3624 1265)
-> (load 'irewrite)
[fasl irewrite.o]
t
-> '(this has the localf declaration)
(this has the localf declaration)
-> (sstatus translink off)
off
-> (setup)
t
-> (test)
(t 3191 1311)
-> (sstatus translink on)
on
-> (test)
(t 3128 1249)
-> (test)
(t 3117 1267)
-> (exit)
713.4u 61.6s 22:26 57% 74+727k 36+2io 208pf+0w
% ↑D
script done on Sat Nov 27 20:57:46 1982
;;; thus it looks like the speedup due to localf's, if status translink is
on, is (3624-3117)/3624 or about 14%. not as large a speedup as I thought.
I might have been messing with status translink set wrong. I haven't
gone back and checked, but I thought Novak's times were, overall, faster.
The declaration looks like this:
(declare (localf
add-lemma add-lemma-lst apply-subst apply-subst-lst falsep one-way-unify
one-way-unify1 one-way-unify1-lst rewrite rewrite-args rewrite-with-lemmas
tautologyp tautp trans-of-implies trans-of-implies1 truep))
;;everything but test and setup is a local function
Mail-from: ARPANET site SU-SCORE rcvd at 28-Nov-82 1528-CST
Date: 28 Nov 1982 1328-PST
From: Gordon Novak <CSD.NOVAK at SU-SCORE>
Subject: Re: my numbers for irewrite
To: Kim.fateman at UCB-C70
cc: cl.boyer at UTEXAS-20, fateman@Kim at SU-SCORE
In-Reply-To: Your message of 27-Nov-82 2107-PST
*** EOOH ***
Date: Sunday, 28 November 1982 15:28-CST
From: Gordon Novak <CSD.NOVAK at SU-SCORE>
To: Kim.fateman at UCB-C70
cc: cl.boyer, fateman at Kim at SU-SCORE
Re: my numbers for irewrite
With the localf declarations added, I get a substantial improvement
in speed. The new numbers are:
Elapsed time Result
1:57 (t 5827 4528)
1:07 (t 2496 1171)
1:00 (t 2520 1198)
0:54 (t 2523 1218)
1:47 (t 2366 1004)
0:44 (t 2191 911)
0:45 (t 2267 962)
0:45 (t 2272 971)
0:44 (t 2267 998)
0:49 (t 2271 1026)
-- (t 2329 1057)
Avg. 2350.2 1051.6
39.17 17.53 seconds
total GC
"translink" seemed to have no effect with the localf declarations in
place, which I suppose is to be expected. This test was run on Opus 38
Franz; these numbers are substantially better than Dick's numbers.
Cheers, Gordon
The ELISP test
[PHOTO: Recording initiated Tue 29-Jun-82 12:23PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4A(67)-1
End of <CL.BOYER>COMAND.CMD.1
@<ELISP>ELISP
[Keeping]
Elisp, 4 27 82
*(DSKIN "EREWRITE.FLAP")
"EREWRITE.FLAP.2"
Files-Loaded
*(SETUP)
T
*(TEST)
19776 msec CPU (7447 msec GC), 41583 msec clock, 452930 words consed
(T)
*(TEST)
18185 msec CPU (6361 msec GC), 51621 msec clock, 452930 words consed
(T)
*↑C
@POP
[PHOTO: Recording terminated Tue 29-Jun-82 12:26PM]
Interlisp bcompl blocklib swap and noswap
[PHOTO: Recording initiated Mon 5-Jul-82 12:16PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4B(70)-1
End of <CL.BOYER>COMAND.CMD.1
@LISP.EXE.133
INTERLISP-10 27-NOV-79 ...
collecting lists
716, 10444 free cells
control-A is an interrupt and can't be an edit control-character
Good afternoon, Bob.
2←LOAD(IREWRITE.COM]
compiled on 5-Jul-82 12:11:29
FILE CREATED 5-Jul-82 12:11:22
IREWRITECOMS
<CL.BOYER.LISPS>IREWRITE.COM.3
3←IREWRITECOMS
((FNS * IREWRITEFNS) (PROP BLKLIBRARYDEF MEMBER SASSOC) (BLOCKS (REWRITEBLOCK
ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY
ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS
SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES
TEST SETUP) (BLKLIBRARY EQUAL MEMBER GETPROP) (GLOBALVARS TEMP-TEMP UNIFY-SUBST)
)))
4←NOSWAPFLG
NIL
5←(MINFS 100000]
10000
6←(RECLAIM]
collecting lists
7245, 92749 free cells, 0 pages left
92749
7←(GCGAG]
40
8←(MINFS 10000]
100000
9←SETUP]
T
10←(TEST]
(T 15821 4995)
11←(TEST]
(T 17498 6245)
12←(TEST]
(T 16569 5954)
13←(TEST]
(T 16707 5925)
14←(SETQ NOSWAPFLG T]
(NOSWAPFLG reset)
T
15←LOAD(IREWRITE.COM]
compiled on 5-Jul-82 12:11:29
FILE CREATED 5-Jul-82 12:11:22
(REWRITEBLOCK redefined)
(TEST redefined)
(SETUP redefined)
IREWRITECOMS
<CL.BOYER.LISPS>IREWRITE.COM.3
16←TEST]
(T 19546 8561)
17←TEST]
(T 17431 6601)
18←TEST]
(T 17192 6511)
19←TEST]
(T 18785 8161)
20←↑C
@POP
[PHOTO: Recording terminated Mon 5-Jul-82 12:29PM]
Interlisp bcompl no blocklib swap and noswap
[PHOTO: Recording initiated Mon 5-Jul-82 12:29PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4B(70)-1
End of <CL.BOYER>COMAND.CMD.1
@LISP.EXE.133
INTERLISP-10 27-NOV-79 ...
collecting lists
716, 10444 free cells
control-A is an interrupt and can't be an edit control-character
Hello, Bob.
2←LOAD(IREWRITE]
FILE CREATED 5-Jul-82 12:11:22
IREWRITECOMS
<CL.BOYER.LISPS>IREWRITE..3
3←IREWRITECOMS
((FNS * IREWRITEFNS) (PROP BLKLIBRARYDEF MEMBER SASSOC) (BLOCKS (REWRITEBLOCK
ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP ONE-WAY-UNIFY
ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS REWRITE-WITH-LEMMAS
SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES TRANS-OF-IMPLIES1 TRUEP (ENTRIES
TEST SETUP) (BLKLIBRARY EQUAL MEMBER GETPROP) (GLOBALVARS TEMP-TEMP UNIFY-SUBST)
)))
4←(BLOCKCOMPILE 'REWRITEBLOCK IREWRITEFNS '(TEST SETUP]
listing? STore and redefine
output file? No
(REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP
ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS
REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES
TRANS-OF-IMPLIES1 TRUEP)
(REWRITEBLOCK (REWRITEBLOCK#0) (TEMP-TEMP UNIFY-SUBST))
collecting lists
6001, 10097 free cells
(TEST NIL NIL)
(TEST redefined)
(SETUP NIL NIL)
(SETUP redefined)
(TEST SETUP)
5←(SETUP]
T
6←(MINFS 100000]
10000
7←(RECLAIM]
collecting lists
9850, 90234 free cells, 0 pages left
90234
8←(MINFS 10000]
100000
9←(GCGAG]
40
10←NOSWAPFLG
NIL
11←(TEST]
(T 31978 6737)
12←(TEST]
(T 47072 6180)
13←(TEST]
LISP Running at 30547 Used 0:10:10.7 in 2:40:39, Load 3.06
(T 71046 6316)
14←(TEST]
LISP Running at 30525 Used 0:11:45.7 in 2:44:33, Load 2.85
(T 71222 7772)
15←(TEST]
(T 70026 6175)
16←(SETQ NOSWAPFLG T]
(NOSWAPFLG reset)
T
17←REDO BLOCKCOMPILE
listing? ST
output file? N
(REWRITEBLOCK ADD-LEMMA ADD-LEMMA-LST APPLY-SUBST APPLY-SUBST-LST FALSEP
ONE-WAY-UNIFY ONE-WAY-UNIFY1 ONE-WAY-UNIFY1-LST PTIME REWRITE REWRITE-ARGS
REWRITE-WITH-LEMMAS SETUP TAUTOLOGYP TAUTP TEST TRANS-OF-IMPLIES
TRANS-OF-IMPLIES1 TRUEP)
(REWRITEBLOCK (REWRITEBLOCK#0) (TEMP-TEMP UNIFY-SUBST))
(REWRITEBLOCK redefined)
(TEST NIL NIL)
(TEST redefined)
(SETUP NIL NIL)
(SETUP redefined)
(TEST SETUP)
18←(TEST]
(T 46501 7685)
19←TEST]
(T 45285 6068)
20←TEST]
(T 46995 7564)
21←TEST]
(T 46522 6180)
22←↑C
@POP
[PHOTO: Recording terminated Mon 5-Jul-82 12:51PM]
Maclisp
[PHOTO: Recording initiated Tue 29-Jun-82 12:26PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4A(67)-1
End of <CL.BOYER>COMAND.CMD.1
@<ATP.MURRAY>MACLSP
LISP 1983
Alloc? Y
# REGPDL = 4000
# SPECPDL = 2000
# FXPDL = 4000
# FLPDL = 1000
LIST = 40000 100000.
SYMBOL = 6000 $
*
(SETQ BASE (SETQ IBASE 10.))
10.
(FASLOAD MREWRITE)
40307.
(SETUP)
T
(TEST)
(T 20190000. 11905000.)
(TEST)
(T 13728000. 5236000.)
(TEST)
(T 13708000. 5398000.)
↑C
@POP
[PHOTO: Recording terminated Tue 29-Jun-82 12:29PM]
**********************************************************************
UCILISP
[PHOTO: Recording initiated Wed 30-Jun-82 12:16PM]
LINK FROM CL.BOYER, TTY 17
Tops-20 Command Processor 4B(70)-1
End of <CL.BOYER>COMAND.CMD.1
@
@ucilsp
UT/UCI LISP - 8/10/80
*(gcgag t)
NIL
*(gc)
3790 FREE STG, 1129 FULL WORDS AVAILABLE
NIL
*(expfs 100000.)
FREE STG EXHAUSTED
FULL WORD SPACE EXHAUSTED
101112 FREE STG, 1131 FULL WORDS AVAILABLE
*(loa≠≠≠≠Jdskin (rewrit.lap))
(ADD-LEMMA 32) (ADD-LEMMA-LST 10) (APPLY-SUBST 23) (APPLY-SUBST-LST 15)
(FALSEP 10) (ONE-WAY-UNIFY 2)
Binary Program Space exceeded
*(expbps 1000)
FREE STG EXHAUSTED
FULL WORD SPACE EXHAUSTED
101012 FREE STG, 1091 FULL WORDS AVAILABLE
*(dskin (rewrit.lap))
(ADD-LEMMA 32) (ADD-LEMMA-LST 10) (APPLY-SUBST 23) (APPLY-SUBST-LST 15)
(FALSEP 10) (ONE-WAY-UNIFY 2) (ONE-WAY-UNIFY1 38) (ONE-WAY-UNIFY1-LST 15)
(REWRITE 20) (REWRITE-ARGS 11) (REWRITE-WITH-LEMMAS 22) (SETUP 2) (TAUTOLOGYP
66) (TAUTP 4) (TEST 2) (TEST1 8) (TRANS-OF-IMPLIES 13) (TRANS-OF-IMPLIES1 31)
(TRUEP 10)
FILES-LOADED
*(setup)
T
*(test)
FREE STG EXHAUSTED
63969 FREE STG, 943 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
47018 FREE STG, 943 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
40438 FREE STG, 943 FULL WORDS AVAILABLE
50614 msec CPU (3738 msec GC), 67496 msec clock, 226465 conses
(T)
*(test)
FREE STG EXHAUSTED
94012 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
58810 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
47089 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
35091 FREE STG, 942 FULL WORDS AVAILABLE
51676 msec CPU (4605 msec GC), 72196 msec clock, 226467 conses
(T)
*(test)
FREE STG EXHAUSTED
91609 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
57005 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
45700 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
34252 FREE STG, 942 FULL WORDS AVAILABLE
52328 msec CPU (4809 msec GC), 70687 msec clock, 226467 conses
(T)
*(nouuo nil)
T
*(test)
FREE STG EXHAUSTED
89843 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
56841 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
45727 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
34117 FREE STG, 942 FULL WORDS AVAILABLE
14099 msec CPU (4711 msec GC), 20077 msec clock, 226467 conses
(T)
*(test)
FREE STG EXHAUSTED
89806 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
56830 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
45727 FREE STG, 942 FULL WORDS AVAILABLE
FREE STG EXHAUSTED
34117 FREE STG, 942 FULL WORDS AVAILABLE
13827 msec CPU (4712 msec GC), 19857 msec clock, 226467 conses
(T)
*
@pop
[PHOTO: Recording terminated Wed 30-Jun-82 12:24PM]
Interlisp (Dolphin and Dorado)
Date: 8 Jul 1982 18:56 PDT
From: JonL at PARC-MAXC
Reply-To: JonL at PARC-MAXC
To: NOVAK at SUMEX-AIM
cc: CL.BOYER, Masinter at PARC-MAXC, LispCore↑ at PARC-MAXC
Re: The Boyer-Moore-Novak Benchmarkings
Gordon, I'll have to apologize for waiting so long to get you the results
of the timing comparisons between your machine and the various
configurations at PARC. I was "laid-low" last Saturday with either a
summer flu, or a severe allergic reaction (hay fever), and couldn't get
the results summarized until yesterday.
I have six areas that I want to summarize in this note:
Translation Inadequacy due to the FreeVars Trip-Up
"Ineffable" Factors Tending to make timing runs Un-Reproducible
PUP Activity -- Ephemeral as well as Ineffable
What the Faster Clock on buys
What DISPLAYDOWN buys
What you can Expect for Dolphin Speed Increases Soon
Briefly, the "FreeVars Trip-Up" and the DISPLAYDOWN account
for most of the sluggishness of the timings you made, but also there's
one "ineffable" which might be sabotaging you.
Below these sections, I've tried to display my data in good scientific
fashion; you'll note that I give a "First run" time and a "Mode run" time.
What this means is the "First run" must absorb all the "ineffable" costs of
swapping in the necessary code and data parts, and of initially-building
the List-space pages that will be used and re-used on subsequent runs.
Also included are one set of timings from a Dorado, just for comparison.
Generally, my comparisons will be of "speed" rather than "time". Thus
if one trial takes 40 secs, and another takes 50 secs, then the first one
runs 25% faster (the other way of saying it would be that the first one
takes 20% less time). The rationale is this: the first one "computes"
.025 MegaFrumbles per second, while the second one only computes
.020 MegaFrumbles per second; hence the speed of the first one is
(.025-.020)/.020 = 25% faster than the speed of the second one.
Translation Inadequacy due to the FreeVars Trip-Up
Actually, it's just as well that I waited until today to report to you,
since the **major factor** in the timings compared so far is the old
"FreeVars Trip-Up", and anyway Boyer's latest modification is more
appropriate for benchmarking, period. I have quite a few interesting
timings to report (and a few remaining mysteries regarding your
machine), but indeed the major discrepancy between your timings
and mine was that the version of IREWRITE we had at Parc is the one
that Larry had "diddled" as per his earlier note.
On your machine, I saw a 50% speedup due to better treatment of the
free variable TEMP-TEMP. (My runs of your original version of
IREWRITE compared with Larry's "diddled" version).
On several machines here, I compared Larry's "diddled" version with
Boyer's new version, and observed about a 9% speed-up of the latter
over the former. Converting TEMP-TEMP from a local variable to a
GLOBALVAR should cause a slowdown in the 1% range (a GLOBALVAR
usage may take time for a GC-hash-table operation, but a LOCALVAR
usage takes time only for pushing/popping the stack) but Boyer changed
several other bottlenecks and the speed increases therefrom more than
compensated for the loss of the local variable (SASSOC ==> FASSOC,
and the placement of important properties at the beginning of the proplist ?)
In any case, this benchmark exhibits a factor of two improvement by
removing what I'm calling the "FreeVars Trip-Up".
This point can't be overstressed: that Interlisp-D is a deep-bound
implementation, whereas MacLisp and current Interlisp-10 are shallow-
bound (Interlisp-10 was first deep-bound, then later shallow-bound),
and that the questionable practice of using free variables for local
temporaries costs little when they are shallow-bound, but could
cost arbitrarily large when deep-bound. I say, "questionable" since a
program with such temporaries is semantically the same regardless of
whether they are GLOBAL, SPECIAL, or local; furthermore, the
general direction of "structured programming" is to avoid free variables
at all costs, and to bind temporaries as syntactically "low" as possible.
The *default* declaration for variables in Interlisp is SPECVARS, for
consistency with the way the interpreter is written, and thus the default
compilation of a free variable will cause a stack scan (slow) rather than a
reference to the global value cell (fast). So one does have to take *some*
action to override the default case when transporting such a program.
A recent Symbolics advertising flyer makes a "comparison" of an Interlisp
program running on the Dolphin and on the LM-2. It wasn't so much
a comparison between Interlisp-D/Dolphin with ZetaLisp/CADR as a
documentation of someone's failure to add the appropriate GLOBALVARS
delcarations. I heard (admittedly, hearsay) that the ISI guy whose program
was under test made the additional declaration himself, and the Dolphin
performance "improved by 67%". [One also wonders how the "comparison"
would have fared had the LISPMachine garbage collector been operable;
a large percentage of the Dolphin time was spent in GC, which helps keep
the working-set small, and also allows you to continue running *after*
the benchmark has finished running.]
"Ineffable" Factors Tending to make timing runs Un-Reproducible
As Larry's note indicated, there is a hidden problem with swap time in
the Interlisp-D of today -- an "ineffable" amount of it is being charged
to CPU time rather than the reported Swap time. The data below seem
to indicate anywhere from 5% to 20% of reported CPU time is really swap
time, when there is indeed swapping going on.
You're quite right, however, that swapping-time is a small factor in this
benchmark; although there consistently seemed to be more of it on your
machine than mine (about 8%, depending on method of interpretation of
the "ineffable" considerations herein mentioned). That's mystery number 1,
since both your machine and mine have the same amount of real memory,
namely about 1.15 Megabyte. The proper setting of RECLAIMMIN keeps
both our Dolphins from "going over the knee" on this benchmark, although
a large setting for my Dolphin caused the CPU time to go up by 50%
and the Swap time to go up from essentially 0 to almost 600 seconds. A
Dorado, with 2 Megabytes and a faster swapping-disk, didn't "go over the
knee" even with the extreme high setting of RECLAIMMIN.
During the first run of TEST, additional pages are added to LIST space,
and the cost of doing this is difficult to estimate accurately in the current
setup. The STATS I ran on the Dorado showed nearly 20% of the
total first-run time given to this activity, but this is inflated by the
fact that the run had to be terminated abnormally (ran out of DSK space
for keeping statistics); this "ineffable" time would concentrate in the
early part of the run. But a 5%-10% slowdown due to this facter seems
indicated in general (my "educated guess" from mulling over the data).
There is a certain oddity about the reference-count GC scheme in that
a call to RECLAIM may not necessarily recover all reclaimable space.
Without going into the details of this oddity, I merely observed that
between TEST runs, it was necessary to do several iterations of
(RECLAIM) before the time spent therein settled down to a typical low
value [indicating that most if not all reclaimables were in fact reclaimed].
This is why I've indicated a "mode" run -- namely the timings that are
most often seen after the initial swap-in, initial swell-up of LIST space,
and "cleanness" of the reclaimable space are accounted for. But I must
confess, that I hadn't discovered all of these things initially, so there is
a little uncertainty about the "mode" timings done on July 2.
PUP Activity -- Ephemeral as well as Ineffable
Mystery number 2 is why the "diddled" TEST run on your machine has
a "mode" of 210 CPU seconds as opposed to about 143 CPU seconds on a
comparably-clocked machine here running the current CONBRIO release.
(This was my measurement for the "diddled" version -- you reported 278
for the original version and I recorded 299. for the original version -- but
the "diddled" version is *exactly* the same file I had at PARC, in the same
release of Lisp).
It's almost as if you had some large overhead activity going on all the time,
such as snarfing up random PUPs and throwing them away. Pup activity
could be a highly-variable thing, and could account for large timing
differences between say Friday afternoon and Thursday morning.
Unfortunately, its also something that is not easily controlled by a user
doing timings, since it depends the PUP activity of others users of the
same ethernet. Currently, time spent in Interlisp-D "dropping" non-
intended PUPs is not visible in the timings statistics (it would merely
bloat reported CPU time). PUP activity could be monitored by another
Dolphin running EtherWatch while you are running timings on yours.
[A simple way of temporarily turning off PUP activity might help
filter out this as a source of variability; are you interested in trying?]
What the Faster Clock on buys
My Dolphin is indeed faster than many others, because it has a clock
crystal running at 44.5 MegaHertz. The Dolphin was originally intended
to run at 50MHz, but due to a larger-than-expected variability in the
components (chips, etc) the production models are currently pegged at
40MHz. Machines with a 44.5MHz clock have a speed increase of about 12% to
16%. The reason why this isn't merely 10% is that there is a "buffering"
action of the constant-time overhead required for maintaining the display
and sampling the keyboard; thus a faster machine spends proportionately
less of its time in these constant overhead tasks. Of course, 50MHz clocks
would result in even more performance improvement.
What DISPLAYDOWN buys
I thought that you had run with DISPLAYDOWN during the compute-
bound TEST; so I ran this way on my runs, except for those intended
to gather data which would correlate the effect of DISPLAYDOWN.
It makes sense to do so on *compute-bound* tasks, since an average
speed increase of 41% to 45% is thereby obtained.
As expected, the display off means more to CPU time on a 40MHz
machine than to that on a 44.5MHz one -- 43% as opposed to only 36%.
GC timings are so variable that I factored them out for these percentages.
[I don't think one would see anything like this gain if the keyboard
sampling mentioned above were similarly shut off; Dorado STATS point
to maybe 6% possible, but even this overhead cost may go down as more
software is developed. As a side comment, display maintenance is not
a significant factor in the Dorado or in the DandeLion.]
What you can Expect for Dolphin Speed Increases Soon
The WIND version of the software will likely be released later this
year, and the data herein indicate a minimum of about 10% overall
increase in speed; other preliminary measures suggest a speed-up of
15% to 20%. Faster hardware may be in the works, but I'm not the one
to comment in any offical way about this. Maybe when we get some
more benchmarks (such as Dick Gabriel is pushing for), we'll do them
on the latest Dolphins.
Just for the record, I'd like to include some timings given me by Larry,
which were done on the Dolphin of one year ago (the "diddled" version
of the problem):
Swap time = 30secs
GC time = 175secs
CPU time = 750secs
Elapsed = 950secs
So today's "vanilla" times are 5.6 times faster than last years, and on my
44.5Mhz machine running WIND I see a speed-up of a factor of 7.
A factor of 7!
Bill van Melle suggests that these speed-ups are due mainly to improvements
in function call and CONS, and that's precisely what the Boyer-Moore
IREWRITE benchmark tests. I really don't think anything quite that dramatic is
on the horizon for the *overall* Dolphin performance, but *selected areas*
which we have targeted for more devolpment could show stellar improvement.
(such as putting floating-point into microcode).
Hope to see you at AAAI.
_________________________________________________
The Raw Data
Machines: GSN (Gordon Novak's), JONL (mine), SYBAL (John Sybalsky's)
[GSN and SYBAL have 40MHz, JONL has 44.5MHz]
Finisterra (the only Dorado included)
Program: OB (Old Boyer code, without declarations)
NB (New Boyer code, with GLOBALVARS for free temps)
Diddled (Larry Masinter's reworking using local lambda
binding for temporaries)
Version: CB (current release CONBRIO), WD (WIND system)
Options: DD (display "down", or off), DU (display "up")
1st (first run), nth ("mode", or most frequently observed after first)
All measurements in seconds. Timings on SYBAL,NB,CB,DD were also
reproduced quite closely on Larry Masinter's machine, and on Stu Card's.
Display Up vs. Display Down times
-----------------------------------------------------------------
Swap 3.6 GSN | Swap 3.0 GSN July 2
GC 66.4 OB | GC 49. OB
CPU 415. CB,DU,nth | CPU 299. CB,DD,nth
Swap 33.1 GSN | Swap 5.7 GSN July 2
GC 70.0 diddled | GC 50.9 diddled
CPU 305. CB,DU,1st | CPU 210. CB,DD,nth
Swap 0.5 JONL | Swap - JONL July 2
GC 60. diddled | GC 30.2 diddled
CPU 158. WD,DU,nth | CPU 116. WD,DD,nth
Swap - SYBAL | Swap - SYBAL July 7
GC 56. diddled | GC 39.6 diddled
CPU 204. CB,DU,nth | CPU 143. CB,DD,nth
First run vs. nth ("mode") run; Display Down
-----------------------------------------------------------------
Swap 2. JONL | Swap - JONL July 7
GC 26.7 NB | GC 31.6 NB
CPU 142. CB,DD,1st | CPU 117. CB,DD,nth
Swap .2 JONL | Swap - JONL July 7
GC 24.9 NB | GC 28.2 NB
CPU 119. WD,DD,1st | CPU 107. WD,DD,nth
Swap 9.8 SYBAL | Swap - SYBAL July 7
GC 31. NB | GC 35. NB
CPU 140. CB,DD,1st | CPU 132. CB,DD,nth
Swap .14 SYBAL | Swap - SYBAL July 7
GC 20.6 NB | GC 31.7 NB
CPU 133. WD,DD,1st | CPU 119. WD,DD,nth
Swap .1 SYBAL | Swap - SYBAL July 7
GC 33.2 diddled | GC 35. diddled
CPU 150. WD,DD,1st | CPU 130. WD,DD,nth
Dorado time
-----------------------------------------------------------------
Swap ? Finisterra | Swap - Finisterra July 2
GC 11.4 diddled | GC 17. diddled
CPU 25.6 WD,1st | CPU 22.7 WD,nth
The STATS file mentioned for Dorado analysis is on the PHYLUM
file server at PARC, file <JONL>TEST.PRINTOUT. Since it's a
lengthy account of an incomplete run, I didn't reproduce it here.
Mail-from: ARPANET site SU-SCORE rcvd at 8-Jul-82 1245-CDT
Date: 8 Jul 1982 1043-PDT
From: Gordon Novak <CSD.NOVAK at SU-SCORE>
To: Masinter at PARC-MAXC, CL.BOYER at UTEXAS-20
cc: JonL at PARC-MAXC
In-Reply-To: Your message of 7-Jul-82 1812-PDT
Date: Thursday, 8 July 1982 12:43-CDT
From: Gordon Novak <CSD.NOVAK at SU-SCORE>
To: Masinter at PARC-MAXC, CL.BOYER
cc: JonL at PARC-MAXC
I reran the test as Larry did, with similar results (included below).
My problem was that I used TCOMPL instead of BCOMPL. I recall being
told by someone that the Dolphin didn't block-compile like Interlisp-10,
so that BCOMPL and TCOMPL did the same thing. Obviously that isn't true;
I should have been more careful. I apologize for raising a ruckus over
a silly mistake; at least I'm glad that the results will be fair to the
Dolphin crowd.
DISPLAYDOWN, as used in Larry's test, totally turns off the display for
the duration. I haven't used it myself, but I understand that it can
get one into funny problemsif e.g. there are errors in the execution
of the program with the display off; I don't know if most users would
find it acceptable to run in this mode.
NIL
Mail-from: ARPANET site PARC-MAXC rcvd at 13-Jul-82 0217-CDT
From: JonL at PARC-MAXC
To: CL.BOYER
cc: JonL at PARC-MAXC
Re: Timings Table for IREWRITE benchmark
Yes, the SYBAL,NB,CB,DD is an appropriate time for the current "vanilla"
Dolphin; but the Dorado timing I reported in the previous note can't be
strictly compared with the others since it was running the "diddled" test
rather than the NewBoyer (NB) test, and was in the WIND release rather
than CONBRIO. [As it happens, the "diddling" had somewhat of a misfeature
in it, which is why I mentioned that NB is a much better benchmark anyway].
Dorado Frontenac, NewBoyer.benchmark(NB),systemCONBRIO(CB)
DisplayDown (DD) times for "mode" (nth) run:
GC = 10.9
CPU = 17.6
DisplayUp (DU) times for "mode" (nth) run:
GC = 11.8
CPU = 19.2
DisplayDown (DD) times for "FirstRun" (1st) run:
Swap = .027
GC = 10.5
CPU = 17.4
It's not clear to me why the "FirstRun" time was faster in these trials -- chalk
it up to "noise", or maybe to the benefits of larger-memory/faster-disk?
∨
←LOAD(IREWRITE.DCOM)
compiled on 8-JUL-82 09:54:44
FILE CREATED 5-Jul-82 12:52:49
IREWRITECOMS
{DSK}IREWRITE.DCOM;2
←(DISPLAYDOWN (TIMEALL (SETUP)))
Elapsed Time = .755 seconds
SWAP time = .582 seconds
CPU Time = .173 seconds
PAGEFAULTS = 12
LISTP
224
T
←(DISPLAYDOWN '(TIMEALL (TEST)))
Elapsed Time = 175.0 seconds
SWAP time = 6.63 seconds
GC time = 31.5 seconds
CPU Time = 137.0 seconds
PAGEFAULTS = 610
SWAPWRITES = 157
FIXP LISTP
311 226469
(T 168388 31471)
←REDO
Elapsed Time = 183.0 seconds
SWAP time = .494 seconds
GC time = 48.7 seconds
CPU Time = 134.0 seconds
PAGEFAULTS = 21
FIXP LISTP
375 226469
(T 182913 48703)
←REDO
Elapsed Time = 188.0 seconds
SWAP time = .078 seconds
GC time = 52.3 seconds
CPU Time = 136.0 seconds
PAGEFAULTS = 2
FIXP LISTP
419 226469
(T 188209 52257)
←REDO
Elapsed Time = 188.0 seconds
SWAP time = .015 seconds
GC time = 51.2 seconds
CPU Time = 137.0 seconds
PAGEFAULTS = 14
FIXP LISTP
401 226469
(T 187906 51188)
←TIMEALL((TEST))
Elapsed Time = 271.0 seconds
SWAP time = .059 seconds
GC time = 75.3 seconds
CPU Time = 195.0 seconds
PAGEFAULTS = 1
FIXP LISTP
420 226469
(T 270715 75315)
←TIMEALL((TEST))
Elapsed Time = 267.0 seconds
SWAP time = .006 seconds
GC time = 73.2 seconds
CPU Time = 194.0 seconds
PAGEFAULTS = 6
FIXP LISTP
402 226469
(T 267145 73153)
←TIMEALL((TEST))
Elapsed Time = 266.0 seconds
GC time = 72.6 seconds
CPU Time = 194.0 seconds
FIXP LISTP
402 226469
(T 266215 72623)
←DRIBBLE]
∨
The INTERLISP VAX test
Mail-from: ARPANET site USC-ISIB rcvd at 23-Jul-82 1108-CDT
Date: 23 Jul 1982 0907-PDT
Sender: RBATES at USC-ISIB
Subject: Re: lisp comparison.
From: Raymond Bates <RBATES at ISIB>
To: CL.BOYER at UTEXAS-20
Cc: CMP.GOOD at UTEXAS-20, ddyer at USC-ISIB, lynch at USC-ISIB,
Cc: Novak at SUMEX-AIM
Message-ID: <[USC-ISIB]23-Jul-82 09:07:07.RBATES>
In-Reply-To: Your message of Thursday, 22 July 1982 13:12-CDT
*** EOOH ***
Date: Friday, 23 July 1982 11:07-CDT
From: Raymond Bates <RBATES at ISIB>
Sender: RBATES at USC-ISIB
To: CL.BOYER
cc: CMP.GOOD, ddyer at USC-ISIB, lynch at USC-ISIB, Novak at SUMEX-AIM
Re: lisp comparison.
Here is the DRIBBLE file of a long run:
NIL
4←(GCGAG NIL]
40
5←LOAD(IREWRITE.v]
compiled on 22-JUL-82 09:22:17
File Created: 5-Jul-82 12:52:49
% warning! this file possibly incompatible!
Compiled by version 3.0 but current version is 2.1
IREWRITECOMS
/lisp/rbates/lisp/IREWRITE.v;2
6←(SETUP]
T
7←(FOR I FROM 1 TO 20 DO (PRINT (TEST ]
(T 76048 0)
(T 76464 0)
(T 76496 0)
(T 76272 0)
(T 89072 4784)
(T 80992 0)
(T 81840 0)
(T 81600 0)
(T 90512 4752)
(T 81904 0)
(T 82032 0)
(T 81248 0)
(T 90512 5456)
(T 80768 0)
(T 80800 0)
(T 80656 0)
(T 91424 5456)
(T 82112 0)
(T 82384 0)
(T 82432 0)
NIL
8←(DRIBBLE]
You many wonder why the cpu time has an extra 10 seconds each
time the system does a gc. The reason is that the system has to
re-hash all the hash array after the gc and time is being charge
to the computation time and not gc time (we will fix that). This
test was done on our 780. Any thing else you would like to see
or known?
/Ray
∨